Let X, Tx, Y, S and f be given.
Assume HTx: topology_on X Tx.
Assume Hfun: function_on f X Y.
Assume HS: subbasis_on Y S.
Assume HpreS: ∀s : set, s ∈ S → preimage_of X f s ∈ Tx.
Set Ty to be the term generated_topology_from_subbasis Y S.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (topology_from_subbasis_is_topology Y S HS).
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 andI to the current goal.
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 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 HSsub: S ⊆ TpreFam.
Let s be given.
Assume Hs: s ∈ S.
We will prove s ∈ TpreFam.
We prove the intermediate claim HSsubPow: S ⊆ 𝒫 Y.
An exact proof term for the current goal is (andEL (S ⊆ 𝒫 Y) (⋃ S = Y) HS).
We prove the intermediate claim HsPowY: s ∈ 𝒫 Y.
An exact proof term for the current goal is (HSsubPow s Hs).
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) s HsPowY (HpreS s Hs)).
We prove the intermediate claim Hmin: Ty ⊆ TpreFam.
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal Y S TpreFam HS HTpre HSsub).
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.
We will prove (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y).
Apply andI to the current goal.
We will prove topology_on X Tx ∧ topology_on Y Ty.
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 will prove preimage_of X f V ∈ Tx.
We prove the intermediate claim HVTpre: V ∈ TpreFam.
An exact proof term for the current goal is (Hmin V HV).
An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ preimage_of X f U0 ∈ Tx) V HVTpre).
∎