Let X and A be given.
Assume HA: basis_on X A.
We will prove generated_topology X A = Intersection_Fam X {T ∈ 𝒫 (𝒫 X)|topology_on X T ∧ A ⊆ T}.
Set Fam to be the term {T ∈ 𝒫 (𝒫 X)|topology_on X T ∧ A ⊆ T}.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ generated_topology X A.
We prove the intermediate claim HUinPower: U ∈ 𝒫 X.
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (generated_topology_subset X A U HU).
An exact proof term for the current goal is (PowerI X U HUsub).
We prove the intermediate claim HUinAllT: ∀T ∈ Fam, U ∈ T.
Let T be given.
Assume HT: T ∈ Fam.
We prove the intermediate claim HTinPowerPower: T ∈ 𝒫 (𝒫 X).
An exact proof term for the current goal is (SepE1 (𝒫 (𝒫 X)) (λT0 ⇒ topology_on X T0 ∧ A ⊆ T0) T HT).
We prove the intermediate claim HTcond: topology_on X T ∧ A ⊆ T.
An exact proof term for the current goal is (SepE2 (𝒫 (𝒫 X)) (λT0 ⇒ topology_on X T0 ∧ A ⊆ T0) T HT).
We prove the intermediate claim HTtop: topology_on X T.
An exact proof term for the current goal is (andEL (topology_on X T) (A ⊆ T) HTcond).
We prove the intermediate claim HAinT: A ⊆ T.
An exact proof term for the current goal is (andER (topology_on X T) (A ⊆ T) HTcond).
We prove the intermediate claim HGenSubT: generated_topology X A ⊆ T.
We prove the intermediate claim HAllAinT: ∀a ∈ A, a ∈ T.
Let a be given.
Assume Ha: a ∈ A.
An exact proof term for the current goal is (HAinT a Ha).
An exact proof term for the current goal is (generated_topology_finer_weak X A T HTtop HAllAinT).
An exact proof term for the current goal is (HGenSubT U HU).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HUinPower HUinAllT).
Let U be given.
Assume HU: U ∈ Intersection_Fam X Fam.
We prove the intermediate claim HGenTop: topology_on X (generated_topology X A).
An exact proof term for the current goal is (lemma_topology_from_basis X A HA).
We prove the intermediate claim HAinGen: A ⊆ generated_topology X A.
Let a be given.
Assume Ha: a ∈ A.
An exact proof term for the current goal is (basis_in_generated X A a HA Ha).
We prove the intermediate claim HGenInFam: generated_topology X A ∈ Fam.
We prove the intermediate claim HGenInPowerPower: generated_topology X A ∈ 𝒫 (𝒫 X).
Apply PowerI to the current goal.
Let V be given.
Assume HV: V ∈ generated_topology X A.
We prove the intermediate claim HVsub: V ⊆ X.
An exact proof term for the current goal is (generated_topology_subset X A V HV).
An exact proof term for the current goal is (PowerI X V HVsub).
An exact proof term for the current goal is (SepI (𝒫 (𝒫 X)) (λT ⇒ topology_on X T ∧ A ⊆ T) (generated_topology X A) HGenInPowerPower (andI (topology_on X (generated_topology X A)) (A ⊆ generated_topology X A) HGenTop HAinGen)).
We prove the intermediate claim HUinAllT: ∀T ∈ Fam, U ∈ T.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HU).
An exact proof term for the current goal is (HUinAllT (generated_topology X A) HGenInFam).
∎