Let x0 of type ι be given.
Apply set_ext with
prim4 (Sing x0),
UPair 0 (Sing x0) leaving 2 subgoals.
Let x1 of type ι be given.
Apply xm with
x0 ∈ x1,
x1 ∈ UPair 0 (Sing x0) leaving 2 subgoals.
Assume H1: x0 ∈ x1.
Apply set_ext with
x1,
Sing x0 leaving 2 subgoals.
Apply PowerE with
Sing x0,
x1.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply SingE with
x0,
x2,
λ x3 x4 . x4 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply L2 with
λ x2 x3 . x3 ∈ UPair 0 (Sing x0).
The subproof is completed by applying UPairI2 with
0,
Sing x0.
Claim L2: x1 = 0
Apply Empty_eq with
x1.
Let x2 of type ι be given.
Assume H2: x2 ∈ x1.
Apply PowerE with
Sing x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Claim L4: x2 = x0
Apply SingE with
x0,
x2.
The subproof is completed by applying L3.
Apply H1.
Apply L4 with
λ x3 x4 . x3 ∈ x1.
The subproof is completed by applying H2.
Apply L2 with
λ x2 x3 . x3 ∈ UPair 0 (Sing x0).
The subproof is completed by applying UPairI1 with
0,
Sing x0.
Let x1 of type ι be given.
Apply UPairE with
x1,
0,
Sing x0,
x1 ∈ prim4 (Sing x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: x1 = 0.
Apply H1 with
λ x2 x3 . x3 ∈ prim4 (Sing x0).
The subproof is completed by applying Empty_In_Power with
Sing x0.
Apply H1 with
λ x2 x3 . x3 ∈ prim4 (Sing x0).
The subproof is completed by applying Self_In_Power with
Sing x0.