Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: 1 ∈ x0.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H2: 68498.. x0 x1.

Assume H3: SNo x2.

Let x3 of type ι be given.

Assume H4: x3 ∈ binunion x1 {SetAdjoin x4 (Sing x0)|x4 ∈ x2}.

Apply binunionE with x1, {(λ x5 . SetAdjoin x5 (Sing x0)) x4|x4 ∈ x2}, x3, ∃ x4 . and (SNo x4) (or (x3 ∈ x4) (∃ x5 . and (x5 ∈ x4) (∃ x6 . and (x6 ∈ ordsucc x0) (and (1 ∈ x6) (x3 = SetAdjoin x5 (Sing x6)))))) leaving 3 subgoals.

The subproof is completed by applying H4.

Assume H5: x3 ∈ x1.

Apply H2 with x3, ∃ x4 . and (SNo x4) (or (x3 ∈ x4) (∃ x5 . and (x5 ∈ x4) (∃ x6 . and (x6 ∈ ordsucc x0) (and (1 ∈ x6) (x3 = SetAdjoin x5 (Sing x6)))))) leaving 2 subgoals.

The subproof is completed by applying H5.

Let x4 of type ι be given.

Assume H6: (λ x5 . and (SNo x5) (or (x3 ∈ x5) (∃ x6 . and (x6 ∈ x5) (∃ x7 . and (x7 ∈ x0) (and (1 ∈ x7) (x3 = SetAdjoin x6 (Sing x7))))))) x4.

Apply H6 with ∃ x5 . and (SNo x5) (or (x3 ∈ x5) (∃ x6 . and (x6 ∈ x5) (∃ x7 . and (x7 ∈ ordsucc x0) (and (1 ∈ x7) (x3 = SetAdjoin x6 (Sing x7)))))).

Assume H7: SNo x4.

Assume H8: or (x3 ∈ x4) (∃ x5 . and (x5 ∈ x4) (∃ x6 . and (x6 ∈ x0) (and (1 ∈ x6) (x3 = SetAdjoin x5 (Sing x6))))).

Let x5 of type ο be given.

Assume H9: ∀ x6 . and (SNo x6) (or (x3 ∈ x6) (∃ x7 . and (x7 ∈ x6) (∃ x8 . and (x8 ∈ ordsucc x0) (and (1 ∈ x8) (x3 = SetAdjoin x7 (Sing x8)))))) ⟶ x5.

Apply H9 with x4.

Apply andI with SNo x4, or (x3 ∈ x4) (∃ x6 . and (x6 ∈ x4) (∃ x7 . and (x7 ∈ ordsucc x0) (and (1 ∈ x7) (x3 = SetAdjoin x6 (Sing x7))))) leaving 2 subgoals.

The subproof is completed by applying H7.

Apply H8 with or (x3 ∈ x4) (∃ x6 . and (x6 ∈ x4) (∃ x7 . and (x7 ∈ ordsucc x0) (and (1 ∈ x7) (x3 = SetAdjoin x6 (Sing x7))))) leaving 2 subgoals.

Assume H10: x3 ∈ x4.

Apply orIL with x3 ∈ x4, ∃ x6 . and ... ....

...

■

Proofgold Proof