Let x0 of type ι be given.
Apply andI with
eps_ x0 ⊆ SNoElts_ (ordsucc x0),
∀ x1 . x1 ∈ ordsucc x0 ⟶ exactly1of2 ((λ x2 . SetAdjoin x2 (Sing 1)) x1 ∈ eps_ x0) (x1 ∈ eps_ x0) leaving 2 subgoals.
Let x1 of type ι be given.
Apply binunionE with
Sing 0,
{(λ x3 . SetAdjoin x3 (Sing 1)) (ordsucc x2)|x2 ∈ x0},
x1,
x1 ∈ SNoElts_ (ordsucc x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply SingE with
0,
x1,
λ x2 x3 . x3 ∈ SNoElts_ (ordsucc x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply binunionI1 with
ordsucc x0,
{(λ x3 . SetAdjoin x3 (Sing 1)) x2|x2 ∈ ordsucc x0},
0.
Apply nat_0_in_ordsucc with
x0.
The subproof is completed by applying L1.
Apply ReplE_impred with
x0,
λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) (ordsucc x2),
x1,
x1 ∈ SNoElts_ (ordsucc x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Apply binunionI2 with
ordsucc x0,
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ ordsucc x0},
x1.
Apply H5 with
λ x3 x4 . x4 ∈ {(λ x6 . SetAdjoin x6 (Sing 1)) x5|x5 ∈ ordsucc x0}.
Apply ReplI with
ordsucc x0,
λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3,
ordsucc x2.
Apply nat_ordsucc_in_ordsucc with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H4.
Let x1 of type ι be given.