Let X, Tx, Y and dY be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Set CXY to be the term continuous_function_space X Tx Y (metric_topology Y dY).
Set S to be the term (compact_convergence_subbasis_metric X Tx Y dY) ∪ {CXY}.
We will prove topology_on CXY (compact_convergence_topology_metric_C X Tx Y dY).
We prove the intermediate claim HS: subbasis_on CXY S.
We will prove S ⊆ 𝒫 CXY ∧ ⋃ S = CXY.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ S.
We will prove s ∈ 𝒫 CXY.
Apply (binunionE' (compact_convergence_subbasis_metric X Tx Y dY) {CXY} s (s ∈ 𝒫 CXY)) to the current goal.
Assume Hsm: s ∈ compact_convergence_subbasis_metric X Tx Y dY.
An exact proof term for the current goal is (SepE1 (𝒫 CXY) (λS0 : set ⇒ ∃C f eps : set, compact_space C (subspace_topology X Tx C) ∧ C ⊆ X ∧ f ∈ CXY ∧ eps ∈ R ∧ Rlt 0 eps ∧ S0 = {g ∈ CXY|∀x : set, x ∈ C → Rlt (apply_fun dY (apply_fun g x,apply_fun f x)) eps}) s Hsm).
Assume HsC: s ∈ {CXY}.
We prove the intermediate claim Hseq: s = CXY.
An exact proof term for the current goal is (SingE CXY s HsC).
rewrite the current goal using Hseq (from left to right).
An exact proof term for the current goal is (PowerI CXY CXY (Subq_ref CXY)).
An exact proof term for the current goal is Hs.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ S.
We will prove f ∈ CXY.
Apply (UnionE_impred S f Hf (f ∈ CXY)) to the current goal.
Let U be given.
Assume HfU: f ∈ U.
Assume HU: U ∈ S.
Apply (binunionE' (compact_convergence_subbasis_metric X Tx Y dY) {CXY} U (f ∈ CXY)) to the current goal.
Assume HUm: U ∈ compact_convergence_subbasis_metric X Tx Y dY.
We prove the intermediate claim HUpow: U ∈ 𝒫 CXY.
An exact proof term for the current goal is (SepE1 (𝒫 CXY) (λS0 : set ⇒ ∃C f0 eps : set, compact_space C (subspace_topology X Tx C) ∧ C ⊆ X ∧ f0 ∈ CXY ∧ eps ∈ R ∧ Rlt 0 eps ∧ S0 = {g ∈ CXY|∀x : set, x ∈ C → Rlt (apply_fun dY (apply_fun g x,apply_fun f0 x)) eps}) U HUm).
An exact proof term for the current goal is (PowerE CXY U HUpow f HfU).
Assume HUC: U ∈ {CXY}.
We prove the intermediate claim HUeq: U = CXY.
An exact proof term for the current goal is (SingE CXY U HUC).
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HfU.
An exact proof term for the current goal is HU.
Let f be given.
Assume Hf: f ∈ CXY.
We prove the intermediate claim HCinS: CXY ∈ S.
An exact proof term for the current goal is (binunionI2 (compact_convergence_subbasis_metric X Tx Y dY) {CXY} CXY (SingI CXY)).
An exact proof term for the current goal is (UnionI S f CXY Hf HCinS).
An exact proof term for the current goal is (topology_from_subbasis_is_topology CXY S HS).
∎