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.

Assume H3: x1 = x2 ⟶ ∀ x4 : ο . x4.

Assume H4: x1 = x3 ⟶ ∀ x4 : ο . x4.

Assume H5: x2 = x3 ⟶ ∀ x4 : ο . x4.

Claim L6: x1 ∈ setminus x0 (Sing x3)

Apply setminusI with x0, Sing x3, x1 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H6: x1 ∈ Sing x3.

Apply H4.

Apply SingE with x3, x1.

The subproof is completed by applying H6.

Claim L7: x2 ∈ setminus x0 (Sing x3)

Apply setminusI with x0, Sing x3, x2 leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H7: x2 ∈ Sing x3.

Apply H5.

Apply SingE with x3, x2.

The subproof is completed by applying H7.

Claim L8: nIn x3 (setminus x0 (Sing x3))

Apply setminus_nIn_I2 with x0, Sing x3, x3.

The subproof is completed by applying SingI with x3.

Claim L9: atleastp u2 (setminus x0 (Sing x3))

Apply unknownprop_70c71962e8fc1b4ddbda71c37aaca8def65b78d5219f1b88a18baeaefa0b7a55 with setminus x0 (Sing x3), x1, x2 leaving 3 subgoals.

The subproof is completed by applying L6.

The subproof is completed by applying L7.

The subproof is completed by applying H3.

Apply unknownprop_20fce6fc7f2e036c1229cbf996632439eddb19cfae541105a83e5be9c65bc111 with x0, x3, λ x4 x5 . atleastp u3 x5 leaving 2 subgoals.

The subproof is completed by applying H2.

Apply unknownprop_11c6158bd93dbd27daaa9a84a43404be6ccbf75f900b1e28dfa453e64ea6c96b with u2, setminus x0 (Sing x3), x3 leaving 2 subgoals.

The subproof is completed by applying L8.

The subproof is completed by applying L9.

■

Proofgold Proof