Let x0 of type ι be given.
Assume H1: 1 ∈ x0.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H6: x5 ∈ x2.
Apply H5 with
λ x6 x7 . (λ x8 . SetAdjoin x8 (Sing x0)) x5 ∈ x6.
Apply binunionI2 with
x1,
{(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x2},
(λ x6 . SetAdjoin x6 (Sing x0)) x5.
Apply ReplI with
x2,
λ x6 . (λ x7 . SetAdjoin x7 (Sing x0)) x6,
x5.
The subproof is completed by applying H6.
Apply binunionE with
x3,
{(λ x7 . SetAdjoin x7 (Sing x0)) x6|x6 ∈ x4},
(λ x6 . SetAdjoin x6 (Sing x0)) x5,
x5 ∈ x4 leaving 3 subgoals.
The subproof is completed by applying L7.
Apply FalseE with
x5 ∈ x4.
Apply unknownprop_b77e4d13156bc801da7c50d615690a07853273eb1e278cd0903fec4370f9e4e2 with
x0,
x3,
x5 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H8.
Apply ReplE_impred with
x4,
λ x6 . (λ x7 . SetAdjoin x7 (Sing x0)) x6,
(λ x6 . SetAdjoin x6 (Sing x0)) x5,
x5 ∈ x4 leaving 2 subgoals.
The subproof is completed by applying H8.
Let x6 of type ι be given.
Assume H9: x6 ∈ x4.
Claim L11: x5 = x6
Apply unknownprop_69efd4cfe2ea5d2354a44349c7af8c918734fcc831898cfc8069b10f87ccbafa with
x0,
x2,
x4,
x5,
x6 leaving 7 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Apply L11 with
λ x7 x8 . x8 ∈ x4.
The subproof is completed by applying H9.