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.

Assume H1: x3 ∈ x0.

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

Assume H3: equip x0 (ordsucc (ordsucc x1)).

Claim L4: setminus x0 (UPair x2 x3) = setminus (setminus x0 (Sing x2)) (Sing x3)

Apply setminus_binunion with x0, Sing x2, Sing x3, λ x4 x5 . setminus x0 (UPair x2 x3) = x4.

set y4 to be setminus x0 (UPair x2 x3)

set y5 to be setminus x1 (binunion (Sing x3) (Sing y4))

Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4

Let x6 of type ι → ο be given.

Assume H4: x6 (setminus x2 (binunion (Sing y4) (Sing y5))).

set y7 to be λ x7 . x6

Apply unknownprop_4b1a7ff1f1af5eade46b5657f25a1ce39a3af58e2fba0b757867e511fb9aacae with y4, y5, λ x8 x9 . y7 (setminus x2 x8) (setminus x2 x9).

The subproof is completed by applying H4.

Let x6 of type ι → ι → ο be given.

Apply L4 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.

Assume H5: x6 y5 y5.

The subproof is completed by applying H5.

Apply L4 with λ x4 x5 . equip x5 x1.

Claim L5: x3 ∈ setminus x0 (Sing x2)

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

The subproof is completed by applying H1.

Assume H5: x3 ∈ Sing x2.

Apply H2.

Let x4 of type ι → ι → ο be given.

Apply SingE with x2, x3, λ x5 x6 . x4 x6 x5.

The subproof is completed by applying H5.

Apply unknownprop_997b324045b1165b0cf38788927ff324ddb3a505c8b91e290586e4dd5480f2bd with setminus x0 (Sing x2), x1, x3 leaving 2 subgoals.

The subproof is completed by applying L5.

Apply unknownprop_997b324045b1165b0cf38788927ff324ddb3a505c8b91e290586e4dd5480f2bd with x0, ordsucc x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

■

Proofgold Proof