Let X and Fam be given.
Assume HFamNonempty: ∃T : set, T ∈ Fam.
Assume HfamTop: ∀T ∈ Fam, topology_on X T.
We will prove topology_on X (Intersection_Fam X Fam).
We will prove Intersection_Fam X Fam ⊆ 𝒫 X ∧ Empty ∈ Intersection_Fam X Fam ∧ X ∈ Intersection_Fam X Fam ∧ (∀UFam ∈ 𝒫 (Intersection_Fam X Fam), ⋃ UFam ∈ Intersection_Fam X Fam) ∧ (∀U ∈ Intersection_Fam X Fam, ∀V ∈ Intersection_Fam X Fam, U ∩ V ∈ Intersection_Fam X Fam).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ Intersection_Fam X Fam.
We will prove U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HU).
We will prove Empty ∈ Intersection_Fam X Fam.
We prove the intermediate claim HEmptyPower: Empty ∈ 𝒫 X.
An exact proof term for the current goal is (Empty_In_Power X).
We prove the intermediate claim HEmptyAllT: ∀T : set, T ∈ Fam → Empty ∈ T.
Let T be given.
Assume HT: T ∈ Fam.
An exact proof term for the current goal is (topology_has_empty X T (HfamTop T HT)).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) Empty HEmptyPower HEmptyAllT).
We will prove X ∈ Intersection_Fam X Fam.
We prove the intermediate claim HXPower: X ∈ 𝒫 X.
An exact proof term for the current goal is (Self_In_Power X).
We prove the intermediate claim HXAllT: ∀T : set, T ∈ Fam → X ∈ T.
Let T be given.
Assume HT: T ∈ Fam.
An exact proof term for the current goal is (topology_has_X X T (HfamTop T HT)).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) X HXPower HXAllT).
Let UFam be given.
Assume HUFamPow: UFam ∈ 𝒫 (Intersection_Fam X Fam).
We will prove ⋃ UFam ∈ Intersection_Fam X Fam.
We prove the intermediate claim HUFamSubInter: UFam ⊆ Intersection_Fam X Fam.
An exact proof term for the current goal is (PowerE (Intersection_Fam X Fam) UFam HUFamPow).
We prove the intermediate claim HUFamSubPowX: UFam ⊆ 𝒫 X.
Let U be given.
Assume HUinUFam: U ∈ UFam.
We prove the intermediate claim HUinInter: U ∈ Intersection_Fam X Fam.
An exact proof term for the current goal is (HUFamSubInter U HUinUFam).
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HUinInter).
We prove the intermediate claim HUnionPower: ⋃ UFam ∈ 𝒫 X.
Apply PowerI to the current goal.
An exact proof term for the current goal is (Union_Power X UFam HUFamSubPowX).
We prove the intermediate claim HUnionAllT: ∀T : set, T ∈ Fam → ⋃ UFam ∈ T.
Let T be given.
Assume HT: T ∈ Fam.
We prove the intermediate claim HTtop: topology_on X T.
An exact proof term for the current goal is (HfamTop T HT).
We prove the intermediate claim HUFamSubT: UFam ⊆ T.
Let U be given.
Assume HUinUFam: U ∈ UFam.
We prove the intermediate claim HUinInter: U ∈ Intersection_Fam X Fam.
An exact proof term for the current goal is (HUFamSubInter U HUinUFam).
We prove the intermediate claim HUinAllT: ∀T0 : set, T0 ∈ Fam → U ∈ T0.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 ⇒ ∀T0 : set, T0 ∈ Fam → U0 ∈ T0) U HUinInter).
An exact proof term for the current goal is (HUinAllT T HT).
We prove the intermediate claim HUFamPowT: UFam ∈ 𝒫 T.
Apply PowerI to the current goal.
An exact proof term for the current goal is HUFamSubT.
An exact proof term for the current goal is (topology_union_axiom X T HTtop UFam HUFamPowT).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) (⋃ UFam) HUnionPower HUnionAllT).
Let U be given.
Assume HU: U ∈ Intersection_Fam X Fam.
Let V be given.
Assume HV: V ∈ Intersection_Fam X Fam.
We will prove U ∩ V ∈ Intersection_Fam X Fam.
We prove the intermediate claim HUinPower: U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HU).
We prove the intermediate claim HVinPower: V ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) V HV).
We prove the intermediate claim HUVPower: U ∩ V ∈ 𝒫 X.
An exact proof term for the current goal is (binintersect_Power X U V HUinPower HVinPower).
We prove the intermediate claim HUVinAllT: ∀T : set, T ∈ Fam → U ∩ V ∈ T.
Let T be given.
Assume HT: T ∈ Fam.
We prove the intermediate claim HTtop: topology_on X T.
An exact proof term for the current goal is (HfamTop T HT).
We prove the intermediate claim HUT: U ∈ T.
An exact proof term for the current goal is ((SepE2 (𝒫 X) (λU0 ⇒ ∀T0 : set, T0 ∈ Fam → U0 ∈ T0) U HU) T HT).
We prove the intermediate claim HVT: V ∈ T.
An exact proof term for the current goal is ((SepE2 (𝒫 X) (λU0 ⇒ ∀T0 : set, T0 ∈ Fam → U0 ∈ T0) V HV) T HT).
An exact proof term for the current goal is (topology_binintersect_axiom X T HTtop U HUT V HVT).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) (U ∩ V) HUVPower HUVinAllT).
∎