Let x0 of type ι → (ι → ο) → ο be given.

Let x1 of type ι → (ι → ο) → ο be given.

Assume H0: ed32f.. x0 x1.

Let x2 of type ι be given.

Assume H1: ordinal x2.

Let x3 of type ι → ο be given.

Assume H2: 8356a.. x0 x2 x3.

Let x4 of type ι be given.

Assume H3: ordinal x4.

Let x5 of type ι → ο be given.

Assume H4: 610d8.. x1 x4 x5.

Apply H2 with 40dde.. x2 x3 x4 x5.

Let x6 of type ι be given.

Assume H5: (λ x7 . and (ordinal x7) (∃ x8 : ι → ο . and (x0 x7 x8) (35b9b.. x2 x3 x7 x8))) x6.

Apply H5 with 40dde.. x2 x3 x4 x5.

Assume H6: ordinal x6.

Assume H7: ∃ x7 : ι → ο . and (x0 x6 x7) (35b9b.. x2 x3 x6 x7).

Apply H7 with 40dde.. x2 x3 x4 x5.

Let x7 of type ι → ο be given.

Assume H8: (λ x8 : ι → ο . and (x0 x6 x8) (35b9b.. x2 x3 x6 x8)) x7.

Apply H8 with 40dde.. x2 x3 x4 x5.

Assume H9: x0 x6 x7.

Assume H10: 35b9b.. x2 x3 x6 x7.

Apply H4 with 40dde.. x2 x3 x4 x5.

Let x8 of type ι be given.

Assume H11: (λ x9 . and (ordinal x9) (∃ x10 : ι → ο . and (x1 x9 x10) (35b9b.. x9 x10 x4 x5))) x8.

Apply H11 with 40dde.. x2 x3 x4 x5.

Assume H12: ordinal x8.

Assume H13: ∃ x9 : ι → ο . and (x1 x8 x9) (35b9b.. x8 x9 x4 x5).

Apply H13 with 40dde.. x2 x3 x4 x5.

Let x9 of type ι → ο be given.

Assume H14: (λ x10 : ι → ο . and (x1 x8 x10) (35b9b.. x8 x10 x4 x5)) x9.

Apply H14 with 40dde.. x2 x3 x4 x5.

Assume H15: x1 x8 x9.

Assume H16: 35b9b.. x8 x9 x4 x5.

Claim L17: 40dde.. x2 x3 x4 x5

...

Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with x4, x2, x5, x3, 40dde.. x2 x3 x4 x5 leaving 4 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H1.

Assume H18: or (40dde.. x4 x5 x2 x3) (and (x4 = x2) (PNoEq_ x4 x5 x3)).

Apply H18 with 40dde.. x2 x3 x4 x5 leaving 2 subgoals.

Assume H19: 40dde.. x4 x5 x2 x3.

Apply unknownprop_ab808d03ac7e78aa83f072ed699b3ccc158aab0a67cf54e5638eb5435d34c11d with x2, x3, 40dde.. x2 x3 x4 x5.

Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x2, x4, x2, x3, x5, x3 leaving 5 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

The subproof is completed by applying H1.

The subproof is completed by applying L17.

The subproof is completed by applying H19.

Assume H19: and (x4 = x2) (PNoEq_ x4 x5 x3).

Apply unknownprop_ab808d03ac7e78aa83f072ed699b3ccc158aab0a67cf54e5638eb5435d34c11d with x4, x5, 40dde.. x2 x3 x4 x5.

Apply unknownprop_81ad141295a808fea0b45ad277e31915f7577f7fce50f799a6434a1b613c1ee0 with x4, x2, x4, x5, x3, x5 leaving 5 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

Apply orIR with 40dde.. x4 x5 x2 x3, and (x4 = x2) (PNoEq_ x4 x5 x3).

The subproof is completed by applying H19.

The subproof is completed by applying L17.

Assume H18: 40dde.. x2 x3 x4 x5.

The subproof is completed by applying H18.

■

Proofgold Proof