Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Let x2 of type ι be given.
Assume H1: x2 ∈ x0.
Apply iffI with
x2 ∈ PSNo x0 x1,
x1 x2 leaving 2 subgoals.
Apply binunionE with
{x3 ∈ x0|x1 x3},
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0,not (x1 x3)},
x2,
x1 x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x2 ∈ {x3 ∈ x0|x1 x3}.
Apply SepE2 with
x0,
x1,
x2.
The subproof is completed by applying H3.
Apply FalseE with
x1 x2.
Apply ReplSepE_impred with
x0,
λ x3 . not (x1 x3),
λ x3 . (λ x4 . SetAdjoin x4 (Sing 1)) x3,
x2,
False leaving 2 subgoals.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Assume H4: x3 ∈ x0.
Apply tagged_notin_ordinal with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H6 with
λ x4 x5 . x4 ∈ x0.
The subproof is completed by applying H1.
Assume H2: x1 x2.
Apply binunionI1 with
{x3 ∈ x0|x1 x3},
{(λ x4 . SetAdjoin x4 (Sing 1)) x3|x3 ∈ x0,not (x1 x3)},
x2.
Apply SepI with
x0,
λ x3 . x1 x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.