Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: x0 ∈ V_ x1.

Claim L1: x0 ∈ famunion x1 (λ x2 . prim4 (V_ x2))

Apply V_eq with x1, λ x2 x3 . x0 ∈ x2.

The subproof is completed by applying H0.

Apply famunionE with x1, λ x2 . prim4 (V_ x2), x0, ∀ x2 : ο . (∀ x3 . x3 ∈ x1 ⟶ x0 ⊆ V_ x3 ⟶ x2) ⟶ x2 leaving 2 subgoals.

The subproof is completed by applying L1.

Let x2 of type ι be given.

Assume H2: and (x2 ∈ x1) (x0 ∈ prim4 (V_ x2)).

Apply H2 with ∀ x3 : ο . (∀ x4 . x4 ∈ x1 ⟶ x0 ⊆ V_ x4 ⟶ x3) ⟶ x3.

Assume H3: x2 ∈ x1.

Assume H4: x0 ∈ prim4 (V_ x2).

Let x3 of type ο be given.

Assume H5: ∀ x4 . x4 ∈ x1 ⟶ x0 ⊆ V_ x4 ⟶ x3.

Apply H5 with x2 leaving 2 subgoals.

The subproof is completed by applying H3.

Apply PowerE with V_ x2, x0.

The subproof is completed by applying H4.

■

Proofgold Proof