Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x2 ∈ x0.
Apply H1 with
equip (setminus x0 (Sing x2)) x1.
Let x3 of type ι → ι be given.
Apply bijE with
x0,
ordsucc x1,
x3,
equip (setminus x0 (Sing x2)) x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3:
∀ x4 . x4 ∈ x0 ⟶ x3 x4 ∈ ordsucc x1.
Assume H4: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Assume H5:
∀ x4 . x4 ∈ ordsucc x1 ⟶ ∃ x5 . and (x5 ∈ x0) (x3 x5 = x4).
Apply equip_tra with
setminus x0 (Sing x2),
setminus (ordsucc x1) (Sing (x3 x2)),
x1 leaving 2 subgoals.
Let x4 of type ο be given.
Apply H6 with
x3.
Apply unknownprop_20ec276501d9ecb91e40cc4525c5a2c0798ab59924056be0d591bc4dcbb72338 with
x0,
ordsucc x1,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply equip_sym with
x1,
setminus (ordsucc x1) (Sing (x3 x2)).
Let x4 of type ο be given.
Apply H6 with
λ x5 . If_i (x5 = x3 x2) x1 x5.
Apply bijI with
x1,
setminus (ordsucc x1) (Sing (x3 x2)),
λ x5 . If_i (x5 = x3 x2) x1 x5 leaving 3 subgoals.
Let x5 of type ι be given.
Assume H7: x5 ∈ x1.
Apply xm with
x5 = x3 x2,
If_i (x5 = x3 x2) x1 x5 ∈ setminus (ordsucc x1) (Sing (x3 x2)) leaving 2 subgoals.
Assume H8: x5 = x3 x2.
Apply If_i_1 with
x5 = x3 x2,
x1,
x5,
λ x6 x7 . x7 ∈ setminus (ordsucc x1) (Sing (x3 x2)) leaving 2 subgoals.
The subproof is completed by applying H8.
Apply setminusI with
ordsucc x1,
Sing (x3 x2),
x1 leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with x1.
Assume H9:
x1 ∈ Sing (x3 x2).
Apply In_irref with
x1.
Apply SingE with
x3 x2,
x1,
λ x6 x7 . x7 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply H8 with
λ x6 x7 . x6 ∈ x1.
The subproof is completed by applying H7.
Assume H8:
not (x5 = x3 x2).
Apply If_i_0 with
x5 = x3 x2,
x1,
x5,
λ x6 x7 . x7 ∈ setminus (ordsucc x1) (Sing (x3 x2)) leaving 2 subgoals.
The subproof is completed by applying H8.
Apply setminusI with
ordsucc x1,
Sing (x3 x2),
x5 leaving 2 subgoals.
Apply ordsuccI1 with
x1,
x5.
The subproof is completed by applying H7.
Assume H9:
x5 ∈ Sing (x3 x2).
Apply H8.
Apply SingE with
x3 x2,
x5.
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H7: x5 ∈ x1.
Let x6 of type ι be given.
Assume H8: x6 ∈ x1.
Apply xm with
x5 = x3 x2,
If_i (x5 = x3 x2) ... ... = ... ⟶ x5 = x6 leaving 2 subgoals.