Let X, Tx, Y, B and f be given.
Assume HTx: topology_on X Tx.
Assume HBasis: basis_on Y B.
Assume Hfun: function_on f X Y.
Assume HpreB: ∀b : set, b ∈ B → preimage_of X f b ∈ Tx.
Set Ty to be the term generated_topology Y B.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (lemma_topology_from_basis Y B HBasis).
Set TpreFam to be the term {U0 ∈ 𝒫 Y|preimage_of X f U0 ∈ Tx} of type set.
We prove the intermediate claim HTpre: topology_on Y TpreFam.
We prove the intermediate claim HsubPow: TpreFam ⊆ 𝒫 Y.
Let U be given.
Assume HU: U ∈ TpreFam.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) U HU).
We prove the intermediate claim Hempty: Empty ∈ TpreFam.
Apply (SepI (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) Empty (Empty_In_Power Y)) to the current goal.
rewrite the current goal using (preimage_of_Empty X f) (from left to right).
An exact proof term for the current goal is (topology_has_empty X Tx HTx).
We prove the intermediate claim HYin: Y ∈ TpreFam.
Apply (SepI (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) Y (Self_In_Power Y)) to the current goal.
rewrite the current goal using (preimage_of_whole X Y f Hfun) (from left to right).
An exact proof term for the current goal is (topology_has_X X Tx HTx).
We prove the intermediate claim Hunion: ∀UFam ∈ 𝒫 TpreFam, ⋃ UFam ∈ TpreFam.
Let UFam be given.
Assume HUFamPow: UFam ∈ 𝒫 TpreFam.
We prove the intermediate claim HUFsub: UFam ⊆ TpreFam.
An exact proof term for the current goal is (PowerE TpreFam UFam HUFamPow).
We prove the intermediate claim HUnionPowY: ⋃ UFam ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃ UFam.
Apply (UnionE_impred UFam y Hy) to the current goal.
Let U be given.
Assume HyU: y ∈ U.
Assume HUUF: U ∈ UFam.
We prove the intermediate claim HUTpre: U ∈ TpreFam.
An exact proof term for the current goal is (HUFsub U HUUF).
We prove the intermediate claim HUPowY: U ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) U HUTpre).
An exact proof term for the current goal is (PowerE Y U HUPowY y HyU).
Apply (SepI (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) (⋃ UFam) HUnionPowY) to the current goal.
rewrite the current goal using (preimage_of_Union X f UFam) (from left to right).
Set PreFam to be the term {preimage_of X f U|U ∈ UFam} of type set.
We prove the intermediate claim HPreFamSub: PreFam ⊆ Tx.
Let W be given.
Assume HW: W ∈ PreFam.
Apply (ReplE_impred UFam (λU0 : set ⇒ preimage_of X f U0) W HW (W ∈ Tx)) to the current goal.
Let U be given.
Assume HUUF: U ∈ UFam.
Assume HWU: W = preimage_of X f U.
We prove the intermediate claim HUTpre: U ∈ TpreFam.
An exact proof term for the current goal is (HUFsub U HUUF).
We prove the intermediate claim HpreU: preimage_of X f U ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) U HUTpre).
rewrite the current goal using HWU (from left to right).
An exact proof term for the current goal is HpreU.
An exact proof term for the current goal is (topology_union_closed X Tx PreFam HTx HPreFamSub).
We prove the intermediate claim Hinter: ∀U ∈ TpreFam, ∀V ∈ TpreFam, U ∩ V ∈ TpreFam.
Let U be given.
Assume HU: U ∈ TpreFam.
Let V be given.
Assume HV: V ∈ TpreFam.
We prove the intermediate claim HUPow: U ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) U HU).
We prove the intermediate claim HVPow: V ∈ 𝒫 Y.
An exact proof term for the current goal is (SepE1 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) V HV).
We prove the intermediate claim HUVPow: U ∩ V ∈ 𝒫 Y.
An exact proof term for the current goal is (binintersect_Power Y U V HUPow HVPow).
Apply (SepI (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) (U ∩ V) HUVPow) to the current goal.
rewrite the current goal using (preimage_of_binintersect X f U V) (from left to right).
We prove the intermediate claim HpreU: preimage_of X f U ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) U HU).
We prove the intermediate claim HpreV: preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) V HV).
An exact proof term for the current goal is (topology_binintersect_closed X Tx (preimage_of X f U) (preimage_of X f V) HTx HpreU HpreV).
We prove the intermediate claim HTpre_def: topology_on Y TpreFam = (TpreFam ⊆ 𝒫 Y ∧ Empty ∈ TpreFam ∧ Y ∈ TpreFam ∧ (∀UFam ∈ 𝒫 TpreFam, ⋃ UFam ∈ TpreFam) ∧ (∀U ∈ TpreFam, ∀V ∈ TpreFam, U ∩ V ∈ TpreFam)).
Use reflexivity.
rewrite the current goal using HTpre_def (from left to right).
Apply and5I to the current goal.
An exact proof term for the current goal is HsubPow.
An exact proof term for the current goal is Hempty.
An exact proof term for the current goal is HYin.
An exact proof term for the current goal is Hunion.
An exact proof term for the current goal is Hinter.
We prove the intermediate claim HBsubPow: B ⊆ 𝒫 Y.
An exact proof term for the current goal is (andEL (B ⊆ 𝒫 Y) (∀x ∈ Y, ∃b ∈ B, x ∈ b) (andEL (B ⊆ 𝒫 Y ∧ (∀x ∈ Y, ∃b ∈ B, x ∈ b)) (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) HBasis)).
We prove the intermediate claim HBsubTpre: ∀b ∈ B, b ∈ TpreFam.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ TpreFam.
We prove the intermediate claim HbPow: b ∈ 𝒫 Y.
An exact proof term for the current goal is (HBsubPow b HbB).
Apply (SepI (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) b HbPow) to the current goal.
An exact proof term for the current goal is (HpreB b HbB).
We prove the intermediate claim HgenSub: Ty ⊆ TpreFam.
An exact proof term for the current goal is (generated_topology_finer_weak Y B TpreFam HTpre HBsubTpre).
We will prove continuous_map X Tx Y Ty f.
We will prove (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y ∧ ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HTy.
An exact proof term for the current goal is Hfun.
Let V be given.
Assume HV: V ∈ Ty.
We prove the intermediate claim HVpre: V ∈ TpreFam.
An exact proof term for the current goal is (HgenSub V HV).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) V HVpre).
∎