Let U be given.
Assume HUT: TransSet U.
Assume HU: ZF_closed U.
Apply ZF_closed_E U HU to the current goal.
Assume HUU HUP HUR.
Let X be given.
Assume HX: X ∈ U.
Let Y be given.
Assume HY: ∀x ∈ X, Y x ∈ U.
We will prove (∏x ∈ X, Y x) ∈ U.
We prove the intermediate claim L1: (∏x ∈ X, Y x) ∈ 𝒫 (𝒫 (∑x ∈ X, ⋃ (Y x))).
An exact proof term for the current goal is Sep_In_Power (𝒫 (∑x ∈ X, ⋃ (Y x))) (λf ⇒ ∀x ∈ X, f x ∈ Y x).
We prove the intermediate claim L2: (𝒫 (𝒫 (∑x ∈ X, ⋃ (Y x)))) ∈ U.
Apply HUP to the current goal.
Apply HUP to the current goal.
Apply ZF_Sigma_closed U HUT HU X HX (λx ⇒ ⋃ (Y x)) to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove ⋃ (Y x) ∈ U.
Apply HUU to the current goal.
An exact proof term for the current goal is HY x Hx.
An exact proof term for the current goal is HUT (𝒫 (𝒫 (∑x ∈ X, ⋃ (Y x)))) L2 (∏x ∈ X, Y x) L1.
∎