Let x0 of type ι → ο be given.

Assume H0: ∃ x1 . and (ordinal x1) (x0 x1).

Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with ∃ x1 . and (and (ordinal x1) (x0 x1)) (∀ x2 . In x2 x1 ⟶ not (x0 x2)).

Assume H1: not (∃ x1 . and (and (ordinal x1) (x0 x1)) (∀ x2 . In x2 x1 ⟶ not (x0 x2))).

Claim L2: ∀ x1 . ordinal x1 ⟶ not (x0 x1)

Apply unknownprop_a136f966a5f32c42970eaa74da643e650a33010b04dec952965730ae1dedc69c with λ x1 . not (x0 x1).

Let x1 of type ι be given.

Assume H2: ordinal x1.

Assume H3: ∀ x2 . In x2 x1 ⟶ not (x0 x2).

Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with x0 x1.

Assume H4: x0 x1.

Apply notE with ∃ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . In x3 x2 ⟶ not (x0 x3)) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ο be given.

Assume H5: ∀ x3 . and (and (ordinal x3) (x0 x3)) (∀ x4 . In x4 x3 ⟶ not (x0 x4)) ⟶ x2.

Apply H5 with x1.

Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with ordinal x1, x0 x1, ∀ x3 . In x3 x1 ⟶ not (x0 x3) leaving 3 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

The subproof is completed by applying H3.

Apply H0 with False.

Let x1 of type ι be given.

Assume H3: (λ x2 . and (ordinal x2) (x0 x2)) x1.

Apply andE with ordinal x1, x0 x1, False leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: ordinal x1.

Assume H5: x0 x1.

Apply notE with x0 x1 leaving 2 subgoals.

Apply L2 with x1.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof