Let U be given.

Assume HU: U ∈ Tx.

An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) U HU).

We will prove Empty ∈ Tx.

We prove the intermediate claim HEmpPow: Empty ∈ 𝒫 X.

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

We prove the intermediate claim HEmpAll: ∀i ∈ ω, (Empty ∩ apply_fun Xi i) ∈ apply_fun Ti i.

Let i be given.

Assume HiO: i ∈ ω.

We prove the intermediate claim Htopi: topology_on (apply_fun Xi i) (apply_fun Ti i).

An exact proof term for the current goal is (Htops i HiO).

rewrite the current goal using (binintersect_Empty_left (apply_fun Xi i)) (from left to right).

An exact proof term for the current goal is (topology_has_empty (apply_fun Xi i) (apply_fun Ti i) Htopi).

An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) Empty HEmpPow HEmpAll).

We will prove X ∈ Tx.

We prove the intermediate claim HXpow: X ∈ 𝒫 X.

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

We prove the intermediate claim HXAll: ∀i ∈ ω, (X ∩ apply_fun Xi i) ∈ apply_fun Ti i.

Let i be given.

Assume HiO: i ∈ ω.

We prove the intermediate claim Htopi: topology_on (apply_fun Xi i) (apply_fun Ti i).

An exact proof term for the current goal is (Htops i HiO).

Set Xi_i to be the term apply_fun Xi i.

We prove the intermediate claim Hsub: Xi_i ⊆ X.

Let x be given.

Assume Hx: x ∈ Xi_i.

We will prove x ∈ X.

Set Fam to be the term {apply_fun Xi j|j ∈ ω}.

We prove the intermediate claim HXdef: X = ⋃ Fam.

Use reflexivity.

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

We prove the intermediate claim HXi_i_in: Xi_i ∈ Fam.

An exact proof term for the current goal is (ReplI ω (λj : set ⇒ apply_fun Xi j) i HiO).

An exact proof term for the current goal is (UnionI Fam x Xi_i Hx HXi_i_in).

We prove the intermediate claim HcapEq: X ∩ Xi_i = Xi_i.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ X ∩ Xi_i.

An exact proof term for the current goal is (binintersectE2 X Xi_i x Hx).

Let x be given.

Assume Hx: x ∈ Xi_i.

We will prove x ∈ X ∩ Xi_i.

Apply binintersectI to the current goal.

An exact proof term for the current goal is (Hsub x Hx).

An exact proof term for the current goal is Hx.

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

An exact proof term for the current goal is (topology_has_X Xi_i (apply_fun Ti i) Htopi).

An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) X HXpow HXAll).

Let UFam be given.

Assume HUFam: UFam ∈ 𝒫 Tx.

We will prove ⋃ UFam ∈ Tx.

We prove the intermediate claim HUFamSub: UFam ⊆ Tx.

An exact proof term for the current goal is (PowerE Tx UFam HUFam).

We prove the intermediate claim HUnionPow: ⋃ UFam ∈ 𝒫 X.

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

Let x be given.

Assume HxU: x ∈ ⋃ UFam.

Apply UnionE_impred UFam x HxU to the current goal.

Let U be given.

Assume HxUin: x ∈ U.

Assume HUin: U ∈ UFam.

We prove the intermediate claim HUinTx: U ∈ Tx.

An exact proof term for the current goal is (HUFamSub U HUin).

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) U HUinTx)).

An exact proof term for the current goal is (HUsubX x HxUin).

We prove the intermediate claim HUnionAll: ∀i ∈ ω, ((⋃ UFam) ∩ apply_fun Xi i) ∈ apply_fun Ti i.

Let i be given.

Assume HiO: i ∈ ω.

Set Xi_i to be the term apply_fun Xi i.

Set Ti_i to be the term apply_fun Ti i.

We prove the intermediate claim Htopi: topology_on Xi_i Ti_i.

An exact proof term for the current goal is (Htops i HiO).

Set VFam to be the term {(U ∩ Xi_i)|U ∈ UFam}.

We prove the intermediate claim HVFamPow: VFam ∈ 𝒫 Ti_i.

Apply PowerI Ti_i VFam to the current goal.

Let V be given.

Assume HV: V ∈ VFam.

Apply (ReplE_impred UFam (λU0 : set ⇒ U0 ∩ Xi_i) V HV (V ∈ Ti_i)) to the current goal.

Let U be given.

Assume HU: U ∈ UFam.

Assume HVeq: V = U ∩ Xi_i.

We prove the intermediate claim HUinTx: U ∈ Tx.

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

We prove the intermediate claim HUiOpen: ∀j ∈ ω, (U ∩ apply_fun Xi j) ∈ apply_fun Ti j.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀j ∈ ω, (U0 ∩ apply_fun Xi j) ∈ apply_fun Ti j) U HUinTx).

We prove the intermediate claim HcapOpen: (U ∩ Xi_i) ∈ Ti_i.

An exact proof term for the current goal is (HUiOpen i HiO).

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

An exact proof term for the current goal is HcapOpen.

We prove the intermediate claim Hdist: ⋃ VFam = (⋃ UFam) ∩ Xi_i.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ ⋃ VFam.

We will prove x ∈ (⋃ UFam) ∩ Xi_i.

Apply UnionE_impred VFam x Hx to the current goal.

Let V be given.

Assume HxV: x ∈ V.

Assume HV: V ∈ VFam.

Apply (ReplE_impred UFam (λU0 : set ⇒ U0 ∩ Xi_i) V HV (x ∈ (⋃ UFam) ∩ Xi_i)) to the current goal.

Let U be given.

Assume HU: U ∈ UFam.

Assume HVeq: V = U ∩ Xi_i.

We prove the intermediate claim HxVcap: x ∈ U ∩ Xi_i.

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

An exact proof term for the current goal is HxV.

Apply binintersectE U Xi_i x HxVcap to the current goal.

Assume HxU HxXi.

Apply binintersectI to the current goal.

An exact proof term for the current goal is (UnionI UFam x U HxU HU).

An exact proof term for the current goal is HxXi.

Let x be given.

Assume Hx: x ∈ (⋃ UFam) ∩ Xi_i.

We will prove x ∈ ⋃ VFam.

We prove the intermediate claim HxU: x ∈ ⋃ UFam.

An exact proof term for the current goal is (binintersectE1 (⋃ UFam) Xi_i x Hx).

We prove the intermediate claim HxXi: x ∈ Xi_i.

An exact proof term for the current goal is (binintersectE2 (⋃ UFam) Xi_i x Hx).

Apply UnionE_impred UFam x HxU to the current goal.

Let U be given.

Assume HxUin: x ∈ U.

Assume HU: U ∈ UFam.

We prove the intermediate claim Hxcap: x ∈ U ∩ Xi_i.

An exact proof term for the current goal is (binintersectI U Xi_i x HxUin HxXi).

We prove the intermediate claim HcapIn: (U ∩ Xi_i) ∈ VFam.

An exact proof term for the current goal is (ReplI UFam (λU0 : set ⇒ U0 ∩ Xi_i) U HU).

An exact proof term for the current goal is (UnionI VFam x (U ∩ Xi_i) Hxcap HcapIn).

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

An exact proof term for the current goal is (topology_union_axiom Xi_i Ti_i Htopi VFam HVFamPow).

An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) (⋃ UFam) HUnionPow HUnionAll).

Let U be given.

Assume HU: U ∈ Tx.

Let V be given.

Assume HV: V ∈ Tx.

We will prove U ∩ V ∈ Tx.

We prove the intermediate claim HUsubX: U ⊆ X.

An exact proof term for the current goal is (PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) U HU)).

We prove the intermediate claim HVsubX: V ⊆ X.

An exact proof term for the current goal is (PowerE X V (SepE1 (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) V HV)).

We prove the intermediate claim HcapPow: U ∩ V ∈ 𝒫 X.

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

Let x be given.

Assume Hx: x ∈ U ∩ V.

We prove the intermediate claim HxU: x ∈ U.

An exact proof term for the current goal is (binintersectE1 U V x Hx).

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

We prove the intermediate claim HcapAll: ∀i ∈ ω, ((U ∩ V) ∩ apply_fun Xi i) ∈ apply_fun Ti i.

Let i be given.

Assume HiO: i ∈ ω.

Set Xi_i to be the term apply_fun Xi i.

Set Ti_i to be the term apply_fun Ti i.

We prove the intermediate claim Htopi: topology_on Xi_i Ti_i.

An exact proof term for the current goal is (Htops i HiO).

We prove the intermediate claim HUi: (U ∩ Xi_i) ∈ Ti_i.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀j ∈ ω, (U0 ∩ apply_fun Xi j) ∈ apply_fun Ti j) U HU i HiO).

We prove the intermediate claim HVi: (V ∩ Xi_i) ∈ Ti_i.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀j ∈ ω, (U0 ∩ apply_fun Xi j) ∈ apply_fun Ti j) V HV i HiO).

We prove the intermediate claim Hassoc: (U ∩ V) ∩ Xi_i = (U ∩ Xi_i) ∩ (V ∩ Xi_i).

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ (U ∩ V) ∩ Xi_i.

Apply binintersectE (U ∩ V) Xi_i x Hx to the current goal.

Assume HxUV HxXi.

Apply binintersectE U V x HxUV to the current goal.

Assume HxU HxV.

Apply binintersectI to the current goal.

An exact proof term for the current goal is (binintersectI U Xi_i x HxU HxXi).

An exact proof term for the current goal is (binintersectI V Xi_i x HxV HxXi).

Let x be given.

Assume Hx: x ∈ (U ∩ Xi_i) ∩ (V ∩ Xi_i).

Apply binintersectE (U ∩ Xi_i) (V ∩ Xi_i) x Hx to the current goal.

Assume HxUXi HxVXi.

Apply binintersectE U Xi_i x HxUXi to the current goal.

Assume HxU HxXi.

Apply binintersectE V Xi_i x HxVXi to the current goal.

Assume HxV HxXi2.

Apply binintersectI to the current goal.

An exact proof term for the current goal is (binintersectI U V x HxU HxV).

An exact proof term for the current goal is HxXi.

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

An exact proof term for the current goal is (topology_binintersect_axiom Xi_i Ti_i Htopi (U ∩ Xi_i) HUi (V ∩ Xi_i) HVi).

An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀i ∈ ω, (U0 ∩ apply_fun Xi i) ∈ apply_fun Ti i) (U ∩ V) HcapPow HcapAll).