Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H1 with
x1 = PSNo x0 (λ x2 . x2 ∈ x1).
Apply set_ext with
x1,
PSNo x0 (λ x2 . x2 ∈ x1) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H4: x2 ∈ x1.
Apply binunionE with
x0,
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0},
x2,
x2 ∈ PSNo x0 (λ x3 . x3 ∈ x1) leaving 3 subgoals.
Apply H2 with
x2.
The subproof is completed by applying H4.
Assume H5: x2 ∈ x0.
Apply binunionI1 with
{x3 ∈ x0|x3 ∈ x1},
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0,nIn x3 x1},
x2.
Apply SepI with
x0,
λ x3 . x3 ∈ x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H4.
Apply ReplE_impred with
x0,
λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3,
x2,
x2 ∈ PSNo x0 (λ x3 . x3 ∈ x1) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x3 of type ι be given.
Assume H6: x3 ∈ x0.
Apply binunionI2 with
{x4 ∈ x0|x4 ∈ x1},
{(λ x5 . SetAdjoin x5 (Sing 1)) x4|x4 ∈ x0,nIn x4 x1},
x2.
Apply H7 with
λ x4 x5 . x5 ∈ {(λ x7 . SetAdjoin x7 (Sing 1)) x6|x6 ∈ x0,nIn x6 x1}.
Assume H8: x3 ∈ x1.
Apply exactly1of2_E with
(λ x4 . SetAdjoin x4 (Sing 1)) x3 ∈ x1,
x3 ∈ x1,
False leaving 3 subgoals.
Apply H3 with
x3.
The subproof is completed by applying H6.
Apply H10.
The subproof is completed by applying H8.
Assume H10: x3 ∈ x1.
Apply H9.
Apply H7 with
λ x4 x5 . x4 ∈ x1.
The subproof is completed by applying H4.
Apply ReplSepI with
x0,
λ x4 . nIn x4 x1,
λ x4 . (λ x5 . SetAdjoin x5 (Sing 1)) x4,
x3 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L8.
Let x2 of type ι be given.
Assume H4:
x2 ∈ PSNo x0 (λ x3 . x3 ∈ x1).
Apply binunionE with
{x3 ∈ x0|x3 ∈ x1},
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0,nIn x3 x1},
x2,
x2 ∈ x1 leaving 3 subgoals.
The subproof is completed by applying H4.
Assume H5: x2 ∈ {x3 ∈ x0|x3 ∈ x1}.
Apply SepE with
x0,
λ x3 . x3 ∈ x1,
x2,
x2 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H5.