Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
∃ x2 . and (x2 ∈ x1) (atleastp x0 (setminus x1 (Sing x2))).
Let x2 of type ι → ι be given.
Apply H1 with
∃ x3 . and (x3 ∈ x1) (atleastp x0 (setminus x1 (Sing x3))).
Assume H2:
∀ x3 . x3 ∈ ordsucc x0 ⟶ x2 x3 ∈ x1.
Assume H3:
∀ x3 . x3 ∈ ordsucc x0 ⟶ ∀ x4 . x4 ∈ ordsucc x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Let x3 of type ο be given.
Apply H4 with
x2 x0.
Apply andI with
x2 x0 ∈ x1,
atleastp x0 (setminus x1 (Sing (x2 x0))) leaving 2 subgoals.
Apply H2 with
x0.
The subproof is completed by applying ordsuccI2 with x0.
Let x4 of type ο be given.
Assume H5:
∀ x5 : ι → ι . and (∀ x6 . x6 ∈ x0 ⟶ x5 x6 ∈ setminus x1 (Sing (x2 x0))) (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x5 x6 = x5 x7 ⟶ x6 = x7) ⟶ x4.
Apply H5 with
x2.
Apply andI with
∀ x5 . x5 ∈ x0 ⟶ x2 x5 ∈ setminus x1 (Sing (x2 x0)),
∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x2 x5 = x2 x6 ⟶ x5 = x6 leaving 2 subgoals.
Let x5 of type ι be given.
Assume H6: x5 ∈ x0.
Apply setminusI with
x1,
Sing (x2 x0),
x2 x5 leaving 2 subgoals.
Apply H2 with
x5.
Apply ordsuccI1 with
x0,
x5.
The subproof is completed by applying H6.
Assume H7:
x2 x5 ∈ Sing (x2 x0).
Apply In_irref with
x0.
Apply H3 with
x5,
x0,
λ x6 x7 . x6 ∈ x0 leaving 4 subgoals.
Apply ordsuccI1 with
x0,
x5.
The subproof is completed by applying H6.
The subproof is completed by applying ordsuccI2 with x0.
Apply SingE with
x2 x0,
x2 x5.
The subproof is completed by applying H7.
The subproof is completed by applying H6.
Let x5 of type ι be given.
Assume H6: x5 ∈ x0.
Let x6 of type ι be given.
Assume H7: x6 ∈ x0.
Apply H3 with
x5,
x6 leaving 2 subgoals.
Apply ordsuccI1 with
x0,
x5.
The subproof is completed by applying H6.
Apply ordsuccI1 with
x0,
x6.
The subproof is completed by applying H7.