Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ∈ x0.
Let x2 of type ι be given.
Assume H1: x2 ∈ x0.
Let x3 of type ι be given.
Assume H2: x3 ∈ x0.
Let x4 of type ι be given.
Assume H3: x4 ∈ x0.
Assume H4: x1 = x2 ⟶ ∀ x5 : ο . x5.
Assume H5: x1 = x3 ⟶ ∀ x5 : ο . x5.
Assume H6: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H7: x1 = x4 ⟶ ∀ x5 : ο . x5.
Assume H8: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H9: x3 = x4 ⟶ ∀ x5 : ο . x5.
Apply setminusI with
x0,
Sing x4,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H10:
x1 ∈ Sing x4.
Apply H7.
Apply SingE with
x4,
x1.
The subproof is completed by applying H10.
Apply setminusI with
x0,
Sing x4,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H11:
x2 ∈ Sing x4.
Apply H8.
Apply SingE with
x4,
x2.
The subproof is completed by applying H11.
Apply setminusI with
x0,
Sing x4,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H12:
x3 ∈ Sing x4.
Apply H9.
Apply SingE with
x4,
x3.
The subproof is completed by applying H12.
Apply setminus_nIn_I2 with
x0,
Sing x4,
x4.
The subproof is completed by applying SingI with x4.
Apply unknownprop_8a21f6cb5fc1714044127ec01eb34af4a43c7190a9ab55c5830d9c24f7e274f6 with
setminus x0 (Sing x4),
x1,
x2,
x3 leaving 6 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
Apply unknownprop_20fce6fc7f2e036c1229cbf996632439eddb19cfae541105a83e5be9c65bc111 with
x0,
x4,
λ x5 x6 . atleastp u4 x6 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_11c6158bd93dbd27daaa9a84a43404be6ccbf75f900b1e28dfa453e64ea6c96b with
u3,
setminus x0 (Sing x4),
x4 leaving 2 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.