Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply H0 with
False.
Assume H1:
∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim4 x0.
Assume H2:
∀ x2 . x2 ∈ prim4 x0 ⟶ ∃ x3 . and (x3 ∈ x0) (x1 x3 = x2).
Apply H2 with
{x2 ∈ x0|nIn x2 (x1 x2)},
False leaving 2 subgoals.
The subproof is completed by applying Sep_In_Power with
x0,
λ x2 . nIn x2 (x1 x2).
Let x2 of type ι be given.
Assume H3:
(λ x3 . and (x3 ∈ x0) (x1 x3 = {x4 ∈ x0|nIn x4 (x1 x4)})) x2.
Apply H3 with
False.
Assume H4: x2 ∈ x0.
Assume H5:
x1 x2 = {x3 ∈ x0|nIn x3 (x1 x3)}.
Assume H6: x2 ∈ x1 x2.
Claim L7:
x2 ∈ {x3 ∈ x0|nIn x3 (x1 x3)}Apply H5 with
λ x3 x4 . x2 ∈ x3.
The subproof is completed by applying H6.
Apply SepE2 with
x0,
λ x3 . nIn x3 (x1 x3),
x2 leaving 2 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying H6.
Apply L6.
Apply H5 with
λ x3 x4 . x2 ∈ x4.
Apply SepI with
x0,
λ x3 . nIn x3 (x1 x3),
x2 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying L6.