Let X, S and T be given.
Assume HS HT HST.
We will prove finer_than T (generated_topology_from_subbasis X S).
We will prove generated_topology_from_subbasis X S ⊆ T.
We will prove generated_topology X (basis_of_subbasis X S) ⊆ T.
Let U be given.
Assume HU: U ∈ generated_topology X (basis_of_subbasis X S).
We will prove U ∈ T.
We prove the intermediate claim HU_def: U ⊆ X ∧ (∀x ∈ U, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U).
We prove the intermediate claim HU_power: U ∈ 𝒫 X.
An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀x ∈ U0, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate claim HUsub_X: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HU_power).
We prove the intermediate claim HU_local: ∀x ∈ U, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 ⇒ ∀x ∈ U0, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U0) U HU).
An exact proof term for the current goal is (andI (U ⊆ X) (∀x ∈ U, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U) HUsub_X HU_local).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (andEL (U ⊆ X) (∀x ∈ U, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U) HU_def).
We prove the intermediate claim HUlocal: ∀x ∈ U, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (andER (U ⊆ X) (∀x ∈ U, ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U) HU_def).
We prove the intermediate claim Hbasis_in_T: ∀b ∈ basis_of_subbasis X S, b ∈ T.
Let b be given.
Assume Hb: b ∈ basis_of_subbasis X S.
We will prove b ∈ T.
Apply (xm (b = X)) to the current goal.
Assume Hb_eq_X: b = X.
We prove the intermediate claim HX_in_T: X ∈ T.
We prove the intermediate claim H1: ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T).
An exact proof term for the current goal is (andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) HT).
We prove the intermediate claim H2: (T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T.
An exact proof term for the current goal is (andEL ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T) H1).
An exact proof term for the current goal is (andER (T ⊆ 𝒫 X ∧ Empty ∈ T) (X ∈ T) H2).
We prove the intermediate claim Hb_in_T_case1: b ∈ T.
rewrite the current goal using Hb_eq_X (from left to right).
An exact proof term for the current goal is HX_in_T.
An exact proof term for the current goal is Hb_in_T_case1.
Assume Hb_ne_X: b ≠ X.
We prove the intermediate claim Hb_finite_inter: b ∈ finite_intersections_of X S.
An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 ⇒ b0 ≠ Empty) b Hb).
We prove the intermediate claim Hex_F: ∃F ∈ finite_subcollections S, b = intersection_of_family X F.
An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF ⇒ intersection_of_family X F) b Hb_finite_inter).
Apply Hex_F to the current goal.
Let F be given.
Assume HF_and_eq.
Apply HF_and_eq to the current goal.
Assume HF: F ∈ finite_subcollections S.
Assume Hb_eq: b = intersection_of_family X F.
We prove the intermediate claim HF_sub_S: F ⊆ S.
We prove the intermediate claim HF_power: F ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 ⇒ finite F0) F HF).
An exact proof term for the current goal is (PowerE S F HF_power).
We prove the intermediate claim HF_finite: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 ⇒ finite F0) F HF).
We prove the intermediate claim HF_sub_T: F ⊆ T.
Let s be given.
Assume Hs: s ∈ F.
We prove the intermediate claim Hs_in_S: s ∈ S.
An exact proof term for the current goal is (HF_sub_S s Hs).
An exact proof term for the current goal is (HST s Hs_in_S).
We prove the intermediate claim HF_in_PowerT: F ∈ 𝒫 T.
Apply PowerI to the current goal.
An exact proof term for the current goal is HF_sub_T.
We prove the intermediate claim Hb_inter_in_T: intersection_of_family X F ∈ T.
An exact proof term for the current goal is (finite_intersection_in_topology X T F HT HF_in_PowerT HF_finite).
We prove the intermediate claim Hb_in_T_case2: b ∈ T.
rewrite the current goal using Hb_eq (from left to right).
An exact proof term for the current goal is Hb_inter_in_T.
An exact proof term for the current goal is Hb_in_T_case2.
Set Fam to be the term {b ∈ basis_of_subbasis X S|b ⊆ U}.
We prove the intermediate claim HU_eq_union: U = ⋃ Fam.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U.
We prove the intermediate claim Hex_b: ∃b ∈ basis_of_subbasis X S, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUlocal x Hx).
Apply Hex_b to the current goal.
Let b be given.
Assume Hb_and_props.
Apply Hb_and_props to the current goal.
Assume Hb_basis: b ∈ basis_of_subbasis X S.
Assume Hxb_and_sub.
Apply Hxb_and_sub to the current goal.
Assume Hxb: x ∈ b.
Assume Hb_sub_U: b ⊆ U.
We prove the intermediate claim Hb_in_Fam: b ∈ Fam.
An exact proof term for the current goal is (SepI (basis_of_subbasis X S) (λb0 ⇒ b0 ⊆ U) b Hb_basis Hb_sub_U).
An exact proof term for the current goal is (UnionI Fam x b Hxb Hb_in_Fam).
Let x be given.
Assume Hx: x ∈ ⋃ Fam.
Apply UnionE_impred Fam x Hx to the current goal.
Let b be given.
Assume Hxb: x ∈ b.
Assume Hb_Fam: b ∈ Fam.
We prove the intermediate claim Hb_sub_U: b ⊆ U.
An exact proof term for the current goal is (SepE2 (basis_of_subbasis X S) (λb0 ⇒ b0 ⊆ U) b Hb_Fam).
An exact proof term for the current goal is (Hb_sub_U x Hxb).
We prove the intermediate claim HFam_sub_T: Fam ⊆ T.
Let b be given.
Assume Hb: b ∈ Fam.
We prove the intermediate claim Hb_basis: b ∈ basis_of_subbasis X S.
An exact proof term for the current goal is (SepE1 (basis_of_subbasis X S) (λb0 ⇒ b0 ⊆ U) b Hb).
An exact proof term for the current goal is (Hbasis_in_T b Hb_basis).
We prove the intermediate claim HFam_in_PowerT: Fam ∈ 𝒫 T.
Apply PowerI to the current goal.
An exact proof term for the current goal is HFam_sub_T.
We prove the intermediate claim HUnion_Fam_in_T: ⋃ Fam ∈ T.
We prove the intermediate claim H1: ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T).
An exact proof term for the current goal is (andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) HT).
We prove the intermediate claim H_union_closure: ∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T.
An exact proof term for the current goal is (andER (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T)) (∀UFam ∈ 𝒫 T, ⋃ UFam ∈ T) H1).
An exact proof term for the current goal is (H_union_closure Fam HFam_in_PowerT).
We prove the intermediate claim HU_in_T: U ∈ T.
rewrite the current goal using HU_eq_union (from left to right).
An exact proof term for the current goal is HUnion_Fam_in_T.
An exact proof term for the current goal is HU_in_T.
∎