Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: ZF_closed x0.

Let x1 of type ο be given.

Assume H1: Union_closed x0 ⟶ Power_closed x0 ⟶ Repl_closed x0 ⟶ x1.

Apply H0 with x1.

Assume H2: and (Union_closed x0) (Power_closed x0).

Assume H3: Repl_closed x0.

Apply H2 with x1.

Assume H4: Union_closed x0.

Assume H5: Power_closed x0.

Apply H1 leaving 3 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

The subproof is completed by applying H3.

■