Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply andI with
PSNo x0 x1 ⊆ SNoElts_ x0,
∀ x2 . x2 ∈ x0 ⟶ exactly1of2 ((λ x3 . SetAdjoin x3 (Sing 1)) x2 ∈ PSNo x0 x1) (x2 ∈ PSNo x0 x1) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H1:
x2 ∈ PSNo x0 x1.
Apply binunionE with
{x3 ∈ x0|x1 x3},
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0,not (x1 x3)},
x2,
x2 ∈ SNoElts_ x0 leaving 3 subgoals.
The subproof is completed by applying H1.
Assume H2: x2 ∈ {x3 ∈ x0|x1 x3}.
Apply SepE with
x0,
x1,
x2,
x2 ∈ SNoElts_ x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3: x2 ∈ x0.
Assume H4: x1 x2.
Apply binunionI1 with
x0,
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0},
x2.
The subproof is completed by applying H3.
Apply ReplSepE_impred with
x0,
λ x3 . not (x1 x3),
λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3,
x2,
x2 ∈ SNoElts_ x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H3: x3 ∈ x0.
Apply binunionI2 with
x0,
{(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x0},
x2.
Apply H5 with
λ x4 x5 . x5 ∈ {(λ x7 . SetAdjoin x7 (Sing 1)) x6|x6 ∈ x0}.
Apply ReplI with
x0,
λ x4 . (λ x5 . SetAdjoin x5 (Sing 1)) x4,
x3.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H1: x2 ∈ x0.
Apply xm with
x1 x2,
exactly1of2 ((λ x3 . SetAdjoin x3 (Sing 1)) x2 ∈ PSNo x0 x1) (x2 ∈ PSNo x0 x1) leaving 2 subgoals.
Assume H3: x1 x2.
Apply exactly1of2_I2 with
(λ x3 . SetAdjoin x3 (Sing 1)) x2 ∈ PSNo x0 x1,
x2 ∈ PSNo x0 x1 leaving 2 subgoals.
Apply binunionE with
{x3 ∈ x0|x1 x3},
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0,not (x1 x3)},
(λ x3 . SetAdjoin x3 (Sing 1)) x2,
False leaving 3 subgoals.
The subproof is completed by applying H4.
Apply SepE with
x0,
x1,
(λ x3 . SetAdjoin x3 (Sing 1)) x2,
False leaving 2 subgoals.
The subproof is completed by applying H5.