Let U be given.

Assume HUT: TransSet U.

Assume HU: ZF_closed U.

Let X be given.

Assume HX: X ∈ U.

Let Y be given.

Assume HY: Y ∈ U.

We will prove ({Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y}) ∈ U.

Apply ZF_binunion_closed U HU to the current goal.

We will prove {Inj0 x|x ∈ X} ∈ U.

Apply ZF_Repl_closed U HU X HX Inj0 to the current goal.

Let x be given.

Assume Hx: x ∈ X.

We will prove Inj0 x ∈ U.

Apply ZF_Inj0_closed U HUT HU x to the current goal.

We will prove x ∈ U.

An exact proof term for the current goal is HUT X HX x Hx.

Apply ZF_Repl_closed U HU Y HY Inj1 to the current goal.

Let y be given.

Assume Hy: y ∈ Y.

We will prove Inj1 y ∈ U.

Apply ZF_Inj1_closed U HUT HU y to the current goal.

We will prove y ∈ U.

An exact proof term for the current goal is HUT Y HY y Hy.

∎