Let X and Fam be given.

Assume HFam: Fam ⊆ 𝒫 X.

We will prove ⋃ Fam ⊆ X.

Let x be given.

Assume Hx: x ∈ ⋃ Fam.

We will prove x ∈ X.

Apply (UnionE_impred Fam x Hx) to the current goal.

Let U be given.

Assume HxU: x ∈ U.

Assume HU: U ∈ Fam.

We prove the intermediate claim HUPower: U ∈ 𝒫 X.

An exact proof term for the current goal is (HFam U HU).

We prove the intermediate claim HUsub: U ⊆ X.

An exact proof term for the current goal is (PowerE X U HUPower).

An exact proof term for the current goal is (HUsub x HxU).

∎