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

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

Let x2 of type ι be given.

Assume H0: ordinal x2.

Let x3 of type ι → ο be given.

Assume H1: ∀ x4 . prim1 x4 x2 ⟶ x3 x4.

Assume H2: ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . x0 x4 x5 ⟶ prim1 x4 x2.

Assume H3: ∀ x4 . prim1 x4 x2 ⟶ x0 x4 x3.

Assume H4: ∀ x4 . ordinal x4 ⟶ ∀ x5 : ι → ο . not (x1 x4 x5).

Apply andI with cae4c.. x0 x2 x3, bc2b0.. x1 x2 x3 leaving 2 subgoals.

Let x4 of type ι be given.

Assume H5: ordinal x4.

Let x5 of type ι → ο be given.

Assume H6: x0 x4 x5.

Claim L7: prim1 x4 x2

Apply H2 with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

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

The subproof is completed by applying H0.

The subproof is completed by applying H5.

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

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

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

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

Apply unknownprop_1c12738cd89f8c615a541c15b6797bba2a5be97ab5e514c9fd76b3fef06e2aa9 with x2, x4, x3, x5, False leaving 4 subgoals.

The subproof is completed by applying H9.

Assume H10: PNoLt_ (d3786.. x2 x4) x3 x5.

Apply PNoLt_E_ with d3786.. x2 x4, x3, x5, False leaving 2 subgoals.

The subproof is completed by applying H10.

Let x6 of type ι be given.

Assume H11: prim1 x6 (d3786.. x2 x4).

Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with x2, x4, x6, PNoEq_ x6 x3 x5 ⟶ not (x3 x6) ⟶ x5 x6 ⟶ False leaving 2 subgoals.

The subproof is completed by applying H11.

Assume H12: prim1 x6 x2.

Assume H13: prim1 x6 x4.

Assume H14: PNoEq_ x6 x3 x5.

Assume H15: not (x3 x6).

Apply FalseE with x5 x6 ⟶ False.

Apply H15.

Apply H1 with x6.

The subproof is completed by applying H12.

Assume H10: prim1 x2 x4.

Apply FalseE with PNoEq_ x2 x3 x5 ⟶ x5 x2 ⟶ False.

Apply unknownprop_f1a526a64fd91875cd825eea7f2e7776b7f0e7be5dcee74dc03af1d7886d1eb6 with x2, x4 leaving 2 subgoals.

The subproof is completed by applying H10.

The subproof is completed by applying L7.

Assume H10: prim1 x4 x2.

Assume H11: PNoEq_ x4 x3 x5.

Assume H12: not (x3 x4).

Apply H12.

Apply H1 with x4.

The subproof is completed by applying L7.

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

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

Assume H10: x2 = x4.

Apply FalseE with PNoEq_ x2 x3 x5 ⟶ 40dde.. x4 x5 x2 x3.

Apply In_irref with x2.

Apply H10 with λ x6 x7 . prim1 x7 x2.

The subproof is completed by applying L7.

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

The subproof is completed by applying H8.

Let x4 of type ι be given.

Assume H5: ordinal x4.

Let x5 of type ι → ο be given.

Assume H6: x1 x4 x5.

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

Apply H4 with x4, x5 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

■

Proofgold Proof