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
atleastp (setminus x0 (Sing x2)) x1.
Let x3 of type ι → ι be given.
Apply H2 with
atleastp (setminus x0 (Sing x2)) x1.
Assume H3:
∀ x4 . x4 ∈ x0 ⟶ x3 x4 ∈ ordsucc x1.
Assume H4: ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Apply atleastp_tra with
setminus x0 (Sing x2),
setminus (ordsucc x1) (Sing (x3 x2)),
x1 leaving 2 subgoals.
Let x4 of type ο be given.
Apply H5 with
x3.
Apply unknownprop_085ebafec807a7a2a3be885b45bd1cb633614843d46ca40af31ed222f04aaeef 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_atleastp with
setminus (ordsucc x1) (Sing (x3 x2)),
x1.
Apply equip_sym with
x1,
setminus (ordsucc x1) (Sing (x3 x2)).
Let x4 of type ο be given.
Apply H5 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 H6: 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 H7: 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 H7.
Apply setminusI with
ordsucc x1,
Sing (x3 x2),
x1 leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with x1.
Assume H8:
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 H8.
Apply H7 with
λ x6 x7 . x6 ∈ x1.
The subproof is completed by applying H6.
Assume H7:
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 H7.
Apply setminusI with
ordsucc x1,
Sing (x3 x2),
x5 leaving 2 subgoals.
Apply ordsuccI1 with
x1,
x5.
The subproof is completed by applying H6.
Assume H8:
x5 ∈ Sing (x3 x2).
Apply H7.
Apply SingE with
x3 x2,
x5.
The subproof is completed by applying H8.
Let x5 of type ι be given.
Assume H6: x5 ∈ x1.
Let x6 of type ι be given.
Assume H7: x6 ∈ x1.
Apply xm with
x5 = x3 x2,
If_i (x5 = x3 x2) x1 x5 = If_i (x6 = x3 x2) x1 x6 ⟶ x5 = x6 leaving 2 subgoals.