Let x0 of type ι be given.
Assume H1:
∀ x1 . x1 ∈ x0 ⟶ ordinal x1.
Let x1 of type ο be given.
Assume H2: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 ∈ x3 ⟶ x3 ∈ x4 ⟶ x1.
Apply unknownprop_b3e91047f76692c2df7eb5955e15ae636bf411ce8b2adc37d0ed519e38c03c5e with
u3,
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying nat_3.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x2 of type ι → ι be given.
Assume H3:
(λ x3 : ι → ι . and (inj u3 x0 x3) (∀ x4 . x4 ∈ u3 ⟶ ∀ x5 . x5 ∈ x4 ⟶ x3 x5 ∈ x3 x4)) x2.
Apply H3 with
x1.
Assume H5:
∀ x3 . x3 ∈ u3 ⟶ ∀ x4 . x4 ∈ x3 ⟶ x2 x4 ∈ x2 x3.
Apply H4 with
x1.
Assume H6:
∀ x3 . x3 ∈ u3 ⟶ x2 x3 ∈ x0.
Assume H7:
∀ x3 . x3 ∈ u3 ⟶ ∀ x4 . x4 ∈ u3 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Apply H2 with
x2 0,
x2 u1,
x2 u2 leaving 5 subgoals.
Apply H6 with
0.
The subproof is completed by applying In_0_3.
Apply H6 with
1.
The subproof is completed by applying In_1_3.
Apply H6 with
2.
The subproof is completed by applying In_2_3.
Apply H5 with
u1,
0 leaving 2 subgoals.
The subproof is completed by applying In_1_3.
The subproof is completed by applying In_0_1.
Apply H5 with
u2,
u1 leaving 2 subgoals.
The subproof is completed by applying In_2_3.
The subproof is completed by applying In_1_2.