Apply ZF_ordsucc_closed with
prim6 (prim6 0),
0 leaving 2 subgoals.
The subproof is completed by applying UnivOf_ZF_closed with
prim6 0.
Apply unknownprop_e747e5ba1c4c5fc029f52d44d14d3be2d06759ee5e8f12e8b1e65810154eb535 with
prim6 (prim6 0),
prim6 0 leaving 3 subgoals.
The subproof is completed by applying UnivOf_TransSet with
prim6 0.
The subproof is completed by applying UnivOf_ZF_closed with
prim6 0.
The subproof is completed by applying UnivOf_In with
prim6 0.
Apply unknownprop_b6fb54fab4516b035f62dacd09064964d22d891fcede06066aa8011a5caac6b6 with
λ x0 . x0 ∈ prim6 (prim6 0).
The subproof is completed by applying L0.