We will prove 𝒫 X ⊆ 𝒫 X ∧ Empty ∈ 𝒫 X ∧ X ∈ 𝒫 X ∧ (∀UFam ∈ 𝒫 (𝒫 X), ⋃ UFam ∈ 𝒫 X) ∧ (∀U ∈ 𝒫 X, ∀V ∈ 𝒫 X, U ∩ V ∈ 𝒫 X).

An exact proof term for the current goal is (Subq_ref (𝒫 X)).

Apply Empty_In_Power to the current goal.

Apply PowerI to the current goal.

An exact proof term for the current goal is (Subq_ref X).

We will prove ∀UFam ∈ 𝒫 (𝒫 X), ⋃ UFam ∈ 𝒫 X.

Let UFam be given.

Assume Hfam: UFam ∈ 𝒫 (𝒫 X).

Apply PowerI X (⋃ UFam) to the current goal.

Let x be given.

Assume HxUnion: x ∈ ⋃ UFam.

Apply UnionE_impred UFam x HxUnion to the current goal.

Let U be given.

Assume HUinx: x ∈ U.

Assume HUinFam: U ∈ UFam.

We prove the intermediate claim HFamSub: UFam ⊆ 𝒫 X.

An exact proof term for the current goal is (iffEL (UFam ∈ 𝒫 (𝒫 X)) (UFam ⊆ 𝒫 X) (PowerEq (𝒫 X) UFam) Hfam).

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

An exact proof term for the current goal is HFamSub U HUinFam.

We prove the intermediate claim HUsub: U ⊆ X.

An exact proof term for the current goal is (iffEL (U ∈ 𝒫 X) (U ⊆ X) (PowerEq X U) HUinPower).

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

We will prove ∀U ∈ 𝒫 X, ∀V ∈ 𝒫 X, U ∩ V ∈ 𝒫 X.

Let U be given.

Assume HU: U ∈ 𝒫 X.

Let V be given.

Assume HV: V ∈ 𝒫 X.

Apply PowerI X (U ∩ V) to the current goal.

Let x be given.

Assume Hxcap: x ∈ U ∩ V.

Apply binintersectE U V x Hxcap to the current goal.

Assume HxU HxV.

We prove the intermediate claim HUsub: U ⊆ X.

An exact proof term for the current goal is (iffEL (U ∈ 𝒫 X) (U ⊆ X) (PowerEq X U) HU).

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