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 H14:
∀ x3 : ι → ι . bij {x4 ∈ x0|ordinal x4} x1 x3 ⟶ x2.
Apply H14 with
In_rec_i (λ x3 . λ x4 : ι → ι . prim0 ((λ x5 . λ x6 : ι → ι . λ x7 . and ((λ x8 x9 . λ x10 : ι → ι . and (x9 ∈ x1) (∀ x11 . x11 ∈ x8 ⟶ x10 x11 = x9 ⟶ ∀ x12 : ο . x12)) x5 x7 x6) (∀ x8 . (λ x9 x10 . λ x11 : ι → ι . and (x10 ∈ x1) (∀ x12 . x12 ∈ x9 ⟶ x11 x12 = x10 ⟶ ∀ x13 : ο . x13)) x5 x8 x6 ⟶ V_ x7 ⊆ V_ x8)) x3 x4)).
Apply and3I with
∀ x3 . x3 ∈ {x4 ∈ x0|ordinal x4} ⟶ In_rec_i (λ x4 . λ x5 : ι → ι . prim0 ((λ 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)) x4 x5)) x3 ∈ x1,
∀ x3 . ... ⟶ ∀ x4 . ... ⟶ In_rec_i (λ x5 . λ x6 : ι → ι . prim0 ((λ 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)) x5 x6)) x3 = In_rec_i (λ x5 . λ x6 : ι → ι . prim0 ((λ 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)) ... ...)) ... ⟶ x3 = x4,
... leaving 3 subgoals.