Let x0 of type ι → ο be given.

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

Apply dneg with ∃ x1 . and (and (ordinal x1) (x0 x1)) (∀ x2 . x2 ∈ x1 ⟶ not (x0 x2)).

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

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

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

Let x1 of type ι be given.

Assume H2: ordinal x1.

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

Assume H4: x0 x1.

Apply H1.

Let x2 of type ο be given.

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

Apply H5 with x1.

Apply and3I with ordinal x1, x0 x1, ∀ x3 . 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 H3 with False.

Assume H4: ordinal x1.

Assume H5: x0 x1.

Apply L2 with x1 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof