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.

Let x4 of type ι → ο be given.

Assume H2: 1a487.. x0 x1 x2 x3.

Assume H3: 47618.. x0 x1 x2 x4.

Apply H1 with ∀ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5).

Assume H4: TransSet x2.

Assume H5: ∀ x5 . prim1 x5 x2 ⟶ TransSet x5.

Apply H2 with ∀ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5).

Assume H6: and (ordinal x2) (47618.. x0 x1 x2 x3).

Apply H6 with (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 : ι → ο . not (47618.. x0 x1 x5 x6)) ⟶ ∀ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5).

Assume H7: ordinal x2.

Assume H8: 47618.. x0 x1 x2 x3.

Assume H9: ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 : ι → ο . not (47618.. x0 x1 x5 x6).

Apply H8 with ∀ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5).

Assume H10: cae4c.. x0 x2 x3.

Assume H11: bc2b0.. x1 x2 x3.

Apply H3 with ∀ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5).

Assume H12: cae4c.. x0 x2 x4.

Assume H13: bc2b0.. x1 x2 x4.

Claim L14: ∀ x5 . ordinal x5 ⟶ prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5)

Apply ordinal_ind with λ x5 . prim1 x5 x2 ⟶ iff (x3 x5) (x4 x5).

Let x5 of type ι be given.

Assume H14: ordinal x5.

Assume H15: ∀ x6 . prim1 x6 x5 ⟶ prim1 x6 x2 ⟶ iff (x3 x6) (x4 x6).

Assume H16: prim1 x5 x2.

Claim L17: ...

...

Apply iffI with x3 x5, x4 x5 leaving 2 subgoals.

Assume H18: x3 x5.

Apply dneg with x4 x5.

Assume H19: not (x4 x5).

Claim L20: 40dde.. x5 x4 x2 x3

...

Claim L21: 40dde.. x2 x4 x5 x4

Apply unknownprop_b51c738b3a14385af55eef02a445728dc056a37996fdc42e5ede8e064af23c97 with x2, x5, x4, x4 leaving 3 subgoals.

The subproof is completed by applying H16.

The subproof is completed by applying PNoEq_ref_ with x5, x4.

The subproof is completed by applying H19.

Apply H9 with x5, x4 leaving 2 subgoals.

The subproof is completed by applying H16.

Apply andI with cae4c.. x0 x5 x4, bc2b0.. x1 x5 x4 leaving 2 subgoals.

Let x6 of type ι be given.

Assume H22: ordinal x6.

Let x7 of type ι → ο be given.

Assume H23: x0 x6 x7.

Apply unknownprop_37f5b5c6ee0011f262b499567d54413188e5bd83bd5555e5f3caca08d2fd472f with x6, x2, x5, x7, x4, x4 leaving 5 subgoals.

The subproof is completed by applying H22.

The subproof is completed by applying H1.

The subproof is completed by applying H14.

Apply H12 with x6, x7 leaving 2 subgoals.

The subproof is completed by applying H22.

The subproof is completed by applying H23.

The subproof is completed by applying L21.

Let x6 of type ι be given.

Assume H22: ordinal x6.

Let x7 of type ι → ο be given.

Assume H23: x1 x6 x7.

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

The subproof is completed by applying H14.

The subproof is completed by applying H1.

The subproof is completed by applying H22.

The subproof is completed by applying L20.

Apply H11 with x6, x7 leaving 2 subgoals.

The subproof is completed by applying H22.

The subproof is completed by applying H23.

...

Let x5 of type ι be given.

Assume H15: prim1 x5 x2.

Apply L14 with x5 leaving 2 subgoals.

Apply ordinal_Hered with x2, x5 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H15.

■

Proofgold Proof