Apply ZF_closed_E with prim6 (prim6 0), ∃ x0 x1 x2 : ι → ι → ι → ι → ι → ι . ∃ x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι . MetaCat_pullback_struct_p (λ x4 . x4 ∈ prim6 (prim6 0)) HomSet (λ x4 . lam_id x4) (λ x4 x5 x6 x7 x8 . lam_comp x4 x7 x8) x0 x1 x2 x3 leaving 2 subgoals.

The subproof is completed by applying UnivOf_ZF_closed with prim6 0.

Assume H0: Union_closed (prim6 (prim6 0)).

Assume H1: Power_closed (prim6 (prim6 0)).

Assume H2: Repl_closed (prim6 (prim6 0)).

Claim L3: ∀ x0 . (λ x1 . x1 ∈ prim6 (prim6 0)) x0 ⟶ ∀ x1 . x1 ⊆ x0 ⟶ (λ x2 . x2 ∈ prim6 (prim6 0)) x1

Let x0 of type ι be given.

Assume H3: x0 ∈ prim6 (prim6 0).

Let x1 of type ι be given.

Assume H4: x1 ⊆ x0.

Apply UnivOf_TransSet with prim6 0, prim4 x0, x1 leaving 2 subgoals.

Apply H1 with x0.

The subproof is completed by applying H3.

Apply PowerI with x0, x1.

The subproof is completed by applying H4.

Claim L4: ∀ x0 . (λ x1 . x1 ∈ prim6 (prim6 0)) x0 ⟶ ∀ x1 . (λ x2 . x2 ∈ prim6 (prim6 0)) x1 ⟶ (λ x2 . x2 ∈ prim6 (prim6 0)) (setprod x0 x1)

Apply unknownprop_168889ac2767512e36c59c4d8bc32e41d805ce681fce6d41f1fc82bd258fd1a7 with prim6 (prim6 0) leaving 2 subgoals.

The subproof is completed by applying UnivOf_TransSet with prim6 0.

The subproof is completed by applying UnivOf_ZF_closed with prim6 0.

Apply unknownprop_a58587398f78cc19e584d164063d8a42566021285e8019a61cbb09a5b9caeb5a with λ x0 . x0 ∈ prim6 (prim6 0) leaving 3 subgoals.

The subproof is completed by applying unknownprop_ea08c803821fdb965d694deab91a57c59674f0d5893e9652ca739817958ed900.

The subproof is completed by applying L3.

The subproof is completed by applying L4.

■

Proofgold Proof