Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0:
x1 ∈ prim6 x0.
Let x2 of type ι be given.
Assume H1: x2 ⊆ x1.
The subproof is completed by applying UnivOf_ZF_closed with x0.
Apply PowerI with
x1,
x2.
The subproof is completed by applying H1.
Apply UnivOf_TransSet with
x0,
prim4 x1,
x2 leaving 2 subgoals.
Apply ZF_Power_closed with
prim6 x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H0.
The subproof is completed by applying L3.