Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H4: x4 ∈ x1.
Apply H3 with
λ x5 x6 . (λ x7 . SetAdjoin x7 (Sing 2)) x4 ∈ x5.
Apply binunionI2 with
x0,
{(λ x6 . SetAdjoin x6 (Sing 2)) x5|x5 ∈ x1},
(λ x5 . SetAdjoin x5 (Sing 2)) x4.
Apply ReplI with
x1,
λ x5 . (λ x6 . SetAdjoin x6 (Sing 2)) x5,
x4.
The subproof is completed by applying H4.
Apply binunionE with
x2,
{(λ x6 . SetAdjoin x6 (Sing 2)) x5|x5 ∈ x3},
(λ x5 . SetAdjoin x5 (Sing 2)) x4,
x4 ∈ x3 leaving 3 subgoals.
The subproof is completed by applying L5.
Apply FalseE with
x4 ∈ x3.
Apply ctagged_notin_SNo with
x2,
x4 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H6.
Apply ReplE_impred with
x3,
λ x5 . (λ x6 . SetAdjoin x6 (Sing 2)) x5,
(λ x5 . SetAdjoin x5 (Sing 2)) x4,
x4 ∈ x3 leaving 2 subgoals.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H7: x5 ∈ x3.
Claim L9: x4 = x5
Apply ctagged_eqE_eq with
x1,
x3,
x4,
x5 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
Apply L9 with
λ x6 x7 . x7 ∈ x3.
The subproof is completed by applying H7.