Let U be given.

Assume HUT: TransSet U.

Assume HU: ZF_closed U.

Apply In_ind to the current goal.

Let X be given.

Assume IH: ∀x ∈ X, x ∈ U → Inj1 x ∈ U.

Assume HX: X ∈ U.

rewrite the current goal using Inj1_eq (from left to right).

We will prove ({Empty} ∪ {Inj1 x|x ∈ X}) ∈ U.

Apply ZF_binunion_closed U HU to the current goal.

Apply ZF_Sing_closed U HU to the current goal.

Apply HUT (𝒫 X) (ZF_Power_closed U HU X HX) Empty (Empty_In_Power X) to the current goal.

Apply ZF_Repl_closed U HU X HX to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Apply IH x Hx to the current goal.

We will prove x ∈ U.

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

∎