Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: SNo x0.

Let x2 of type ι be given.

Assume H1: x2 ∈ x0.

Let x3 of type ο be given.

Assume H2: ∀ x4 . and (SNo x4) (or (x2 ∈ x4) (∃ x5 . and (x5 ∈ x4) (∃ x6 . and (x6 ∈ x1) (and (1 ∈ x6) (x2 = SetAdjoin x5 (Sing x6)))))) ⟶ x3.

Apply H2 with x0.

Apply andI with SNo x0, or (x2 ∈ x0) (∃ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x1) (and (1 ∈ x5) (x2 = SetAdjoin x4 (Sing x5))))) leaving 2 subgoals.

The subproof is completed by applying H0.

Apply orIL with x2 ∈ x0, ∃ x4 . and (x4 ∈ x0) (∃ x5 . and (x5 ∈ x1) (and (1 ∈ x5) (x2 = SetAdjoin x4 (Sing x5)))).

The subproof is completed by applying H1.

■

Proofgold Proof