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 Scc to be the term (compact_convergence_subbasis_metric X Tx Y dY) ∪ {CXY}.
We will prove subbasis_on CXY Scc.
We will prove Scc ⊆ 𝒫 CXY ∧ ⋃ Scc = CXY.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ Scc.
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 ∈ ⋃ Scc.
We will prove f ∈ CXY.
Apply (UnionE_impred Scc f Hf (f ∈ CXY)) to the current goal.
Let U be given.
Assume HfU: f ∈ U.
Assume HU: U ∈ Scc.
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 will prove f ∈ ⋃ Scc.
We prove the intermediate claim HCXYin: CXY ∈ Scc.
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 Scc f CXY Hf HCXYin).
∎