Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x2 ∈ x0.
Let x3 of type ι → ι be given.
Apply H1 with
bij (setminus x0 (Sing x2)) (setminus x1 (Sing (x3 x2))) x3.
Assume H2:
and (∀ x4 . x4 ∈ x0 ⟶ x3 x4 ∈ x1) (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5).
Apply H2 with
(∀ x4 . x4 ∈ x1 ⟶ ∃ x5 . and (x5 ∈ x0) (x3 x5 = x4)) ⟶ bij (setminus x0 (Sing x2)) (setminus x1 (Sing (x3 x2))) x3.
Assume H3: ∀ x4 . x4 ∈ x0 ⟶ x3 x4 ∈ x1.
Assume H4: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Assume H5:
∀ x4 . x4 ∈ x1 ⟶ ∃ x5 . and (x5 ∈ x0) (x3 x5 = x4).
Apply bijI with
setminus x0 (Sing x2),
setminus x1 (Sing (x3 x2)),
x3 leaving 3 subgoals.
Let x4 of type ι be given.
Apply setminusE with
x0,
Sing x2,
x4,
x3 x4 ∈ setminus x1 (Sing (x3 x2)) leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: x4 ∈ x0.
Apply setminusI with
x1,
Sing (x3 x2),
x3 x4 leaving 2 subgoals.
Apply H3 with
x4.
The subproof is completed by applying H7.
Assume H9:
x3 x4 ∈ Sing (x3 x2).
Apply H8.
Claim L10: x4 = x2
Apply H4 with
x4,
x2 leaving 3 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H0.
Apply SingE with
x3 x2,
x3 x4.
The subproof is completed by applying H9.
Apply L10 with
λ x5 x6 . x6 ∈ Sing x2.
The subproof is completed by applying SingI with x2.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply H4 with
x4,
x5 leaving 2 subgoals.
Apply setminusE1 with
x0,
Sing x2,
x4.
The subproof is completed by applying H6.
Apply setminusE1 with
x0,
Sing x2,
x5.
The subproof is completed by applying H7.
Let x4 of type ι be given.
Apply setminusE with
x1,
Sing (x3 x2),
x4,
∃ x5 . and (x5 ∈ setminus x0 (Sing x2)) (x3 x5 = x4) leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: x4 ∈ x1.
Apply H5 with
x4,
∃ x5 . and (x5 ∈ setminus x0 (Sing x2)) (x3 x5 = x4) leaving 2 subgoals.
The subproof is completed by applying H7.
Let x5 of type ι be given.
Assume H9:
(λ x6 . and (x6 ∈ x0) (x3 x6 = x4)) x5.