Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: x1 ⊆ x0.
Apply ZF_closed_E with
x0,
∃ x2 : ι → ι . bij {x3 ∈ x0|ordinal x3} x1 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ο be given.
Assume H10:
∀ x3 : ι → ι . bij {x4 ∈ x0|ordinal x4} x1 x3 ⟶ x2.
Apply H10 with
In_rec_i (λ x3 . λ x4 : ι → ι . prim0 (λ x5 . (λ x6 . λ x7 : ι → ι . λ x8 . and ((λ x9 x10 . λ x11 : ι → ι . and (x10 ∈ x1) (∀ x12 . x12 ∈ x9 ⟶ x11 x12 = x10 ⟶ ∀ x13 : ο . x13)) x6 x8 x7) (∀ x9 . (λ x10 x11 . λ x12 : ι → ι . and (x11 ∈ x1) (∀ x13 . x13 ∈ x10 ⟶ x12 x13 = x11 ⟶ ∀ x14 : ο . x14)) x6 x9 x7 ⟶ V_ x8 ⊆ V_ x9)) x3 x4 x5)).
Apply and3I with
∀ x3 . x3 ∈ {x4 ∈ x0|ordinal x4} ⟶ In_rec_i (λ x4 . λ x5 : ι → ι . prim0 (λ x6 . (λ x7 . λ x8 : ι → ι . λ x9 . and ((λ x10 x11 . λ x12 : ι → ι . and (x11 ∈ x1) (∀ x13 . x13 ∈ x10 ⟶ x12 x13 = x11 ⟶ ∀ x14 : ο . x14)) x7 x9 x8) (∀ x10 . (λ x11 x12 . λ x13 : ι → ι . and (x12 ∈ x1) (∀ x14 . x14 ∈ x11 ⟶ x13 x14 = x12 ⟶ ∀ x15 : ο . x15)) x7 x10 x8 ⟶ V_ x9 ⊆ V_ x10)) x4 x5 x6)) x3 ∈ x1,
∀ x3 . ... ⟶ ∀ x4 . ... ⟶ In_rec_i (λ x5 . λ x6 : ι → ι . prim0 (λ x7 . (λ x8 . λ x9 : ι → ι . λ x10 . and ((λ x11 x12 . λ x13 : ι → ι . and (x12 ∈ x1) (∀ x14 . x14 ∈ x11 ⟶ x13 x14 = x12 ⟶ ∀ x15 : ο . x15)) x8 x10 x9) (∀ x11 . (λ x12 x13 . λ x14 : ι → ι . and (x13 ∈ x1) (∀ x15 . x15 ∈ x12 ⟶ x14 x15 = x13 ⟶ ∀ x16 : ο . x16)) x8 x11 x9 ⟶ V_ x10 ⊆ V_ x11)) x5 x6 x7)) x3 = In_rec_i (λ x5 . λ x6 : ι → ι . prim0 (λ x7 . (λ x8 . λ x9 : ι → ι . λ x10 . and ((λ x11 x12 . λ x13 : ι → ι . and (x12 ∈ x1) (∀ x14 . x14 ∈ x11 ⟶ x13 x14 = x12 ⟶ ∀ x15 : ο . x15)) x8 x10 x9) (∀ x11 . (λ x12 x13 . λ x14 : ι → ι . and (x13 ∈ x1) (∀ x15 . x15 ∈ x12 ⟶ x14 x15 = x13 ⟶ ∀ x16 : ο . x16)) ... ... ... ⟶ V_ x10 ⊆ V_ x11)) ... ... ...)) ... ⟶ x3 = x4,
... leaving 3 subgoals.