Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2:
∀ x2 . x2 ∈ x1 ⟶ ordinal x2.
Let x2 of type ο be given.
Assume H3:
∀ x3 x4 . equip x0 x3 ⟶ x4 ∈ x1 ⟶ x3 ⊆ x1 ⟶ x3 ⊆ x4 ⟶ x2.
Apply unknownprop_b3e91047f76692c2df7eb5955e15ae636bf411ce8b2adc37d0ed519e38c03c5e with
ordsucc x0,
x1,
x2 leaving 4 subgoals.
Apply nat_ordsucc with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Let x3 of type ι → ι be given.
Assume H4:
(λ x4 : ι → ι . and (inj (ordsucc x0) x1 x4) (∀ x5 . x5 ∈ ordsucc x0 ⟶ ∀ x6 . x6 ∈ x5 ⟶ x4 x6 ∈ x4 x5)) x3.
Apply H4 with
x2.
Assume H6:
∀ x4 . x4 ∈ ordsucc x0 ⟶ ∀ x5 . x5 ∈ x4 ⟶ x3 x5 ∈ x3 x4.
Apply H5 with
x2.
Assume H7:
∀ x4 . x4 ∈ ordsucc x0 ⟶ x3 x4 ∈ x1.
Assume H8:
∀ x4 . x4 ∈ ordsucc x0 ⟶ ∀ x5 . x5 ∈ ordsucc x0 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Apply H3 with
{x3 x4|x4 ∈ x0},
x3 x0 leaving 4 subgoals.
Apply unknownprop_6f924010899e62355200d41f1cef23d6373bef28ff540d0bdb872dcb6e86d39f with
x0,
x3.
Let x4 of type ι be given.
Assume H9: x4 ∈ x0.
Let x5 of type ι be given.
Assume H10: x5 ∈ x0.
Apply H8 with
x4,
x5 leaving 2 subgoals.
Apply ordsuccI1 with
x0,
x4.
The subproof is completed by applying H9.
Apply ordsuccI1 with
x0,
x5.
The subproof is completed by applying H10.
Apply H7 with
x0.
The subproof is completed by applying ordsuccI2 with x0.
Let x4 of type ι be given.
Assume H9: x4 ∈ {x3 x5|x5 ∈ x0}.
Apply ReplE_impred with
x0,
x3,
x4,
x4 ∈ x1 leaving 2 subgoals.
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H10: x5 ∈ x0.
Assume H11: x4 = x3 x5.
Apply H11 with
λ x6 x7 . x7 ∈ x1.
Apply H7 with
x5.
Apply ordsuccI1 with
x0,
x5.
The subproof is completed by applying H10.
Let x4 of type ι be given.
Assume H9: x4 ∈ {x3 x5|x5 ∈ x0}.
Apply ReplE_impred with
x0,
x3,
x4,
x4 ∈ x3 x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H10: x5 ∈ x0.
Assume H11: x4 = x3 x5.
Apply H11 with
λ x6 x7 . x7 ∈ x3 x0.
Apply H6 with
x0,
x5 leaving 2 subgoals.
The subproof is completed by applying ordsuccI2 with x0.
The subproof is completed by applying H10.