Let x0 of type ι → ο be given.
Assume H0: ∀ x1 . x0 x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ x0 x2.
Apply ZF_closed_E with
prim6 (prim6 0),
∃ x1 x2 : ι → ι → ι → ι → ι . ∃ x3 : ι → ι → ι → ι → ι → ι → ι . MetaCat_equalizer_struct_p (λ x4 . x4 ∈ prim6 (prim6 0)) HomSet (λ x4 . lam_id x4) (λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8) x1 x2 x3 leaving 2 subgoals.
The subproof is completed by applying UnivOf_ZF_closed with
prim6 0.
Claim L4:
∀ x1 . (λ x2 . x2 ∈ prim6 (prim6 0)) x1 ⟶ ∀ x2 . x2 ⊆ x1 ⟶ (λ x3 . x3 ∈ prim6 (prim6 0)) x2Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H5: x2 ⊆ x1.
Apply UnivOf_TransSet with
prim6 0,
prim4 x1,
x2 leaving 2 subgoals.
Apply H2 with
x1.
The subproof is completed by applying H4.
Apply PowerI with
x1,
x2.
The subproof is completed by applying H5.
Apply unknownprop_ddd882da3ecb083533c5169d9ba0d589c2851738e8d8ddd48b103e4363b8bfa8 with
λ x1 . x1 ∈ prim6 (prim6 0).
The subproof is completed by applying L4.