Let X, Tx, Y and dY be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Set Ty to be the term metric_topology Y dY.
Set Dom to be the term function_space X Y.
Set S to be the term compact_open_subbasis X Tx Y Ty.
Set B to be the term basis_of_subbasis Dom S.
Set CXY to be the term continuous_function_space X Tx Y Ty.
Set Tco to be the term compact_open_topology_C X Tx Y Ty.
Set Tcc to be the term compact_convergence_topology_metric_C X Tx Y dY.
We will prove Tco ⊆ Tcc.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
We prove the intermediate claim HSsub: subbasis_on Dom S.
An exact proof term for the current goal is (compact_open_subbasis_is_subbasis X Tx Y Ty HTx HTy).
We prove the intermediate claim HBasisDom: basis_on Dom B.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis Dom S HSsub).
We prove the intermediate claim HCsub: CXY ⊆ Dom.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty).
We prove the intermediate claim HTdom: topology_on Dom (generated_topology Dom B).
An exact proof term for the current goal is (lemma_topology_from_basis Dom B HBasisDom).
We prove the intermediate claim HBpack: basis_on Dom B ∧ generated_topology Dom B = generated_topology_from_subbasis Dom S.
Apply andI to the current goal.
An exact proof term for the current goal is HBasisDom.
Use reflexivity.
We prove the intermediate claim HsubspaceEq: generated_topology CXY {b0 ∩ CXY|b0 ∈ B} = subspace_topology Dom (generated_topology_from_subbasis Dom S) CXY.
An exact proof term for the current goal is (andER (basis_on CXY {b0 ∩ CXY|b0 ∈ B}) (generated_topology CXY {b0 ∩ CXY|b0 ∈ B} = subspace_topology Dom (generated_topology_from_subbasis Dom S) CXY) (subspace_basis Dom (generated_topology_from_subbasis Dom S) CXY B (topology_from_subbasis_is_topology Dom S HSsub) HCsub HBpack)).
We prove the intermediate claim HcoEq: Tco = generated_topology CXY {b0 ∩ CXY|b0 ∈ B}.
rewrite the current goal using (andER (basis_on CXY {b0 ∩ CXY|b0 ∈ B}) (generated_topology CXY {b0 ∩ CXY|b0 ∈ B} = subspace_topology Dom (generated_topology_from_subbasis Dom S) CXY) (subspace_basis Dom (generated_topology_from_subbasis Dom S) CXY B (topology_from_subbasis_is_topology Dom S HSsub) HCsub HBpack)) (from left to right).
Use reflexivity.
We prove the intermediate claim HTcc: topology_on CXY Tcc.
An exact proof term for the current goal is (compact_convergence_topology_metric_C_is_topology X Tx Y dY HTx HdY).
We prove the intermediate claim HgensInTcc: ∀b ∈ {b0 ∩ CXY|b0 ∈ B}, b ∈ Tcc.
Let b be given.
Assume Hb: b ∈ {b0 ∩ CXY|b0 ∈ B}.
We prove the intermediate claim Hexb0: ∃b0 ∈ B, b = b0 ∩ CXY.
An exact proof term for the current goal is (ReplE B (λb1 : set ⇒ b1 ∩ CXY) b Hb).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0pair.
We prove the intermediate claim Hb0B: b0 ∈ B.
An exact proof term for the current goal is (andEL (b0 ∈ B) (b = b0 ∩ CXY) Hb0pair).
We prove the intermediate claim Hbeq: b = b0 ∩ CXY.
An exact proof term for the current goal is (andER (b0 ∈ B) (b = b0 ∩ CXY) Hb0pair).
rewrite the current goal using Hbeq (from left to right).
We prove the intermediate claim Hb0FinInt: b0 ∈ finite_intersections_of Dom S.
An exact proof term for the current goal is (SepE1 (finite_intersections_of Dom S) (λu : set ⇒ u ≠ Empty) b0 Hb0B).
We prove the intermediate claim Hb0ne: b0 ≠ Empty.
An exact proof term for the current goal is (SepE2 (finite_intersections_of Dom S) (λu : set ⇒ u ≠ Empty) b0 Hb0B).
We prove the intermediate claim HexF: ∃F ∈ finite_subcollections S, b0 = intersection_of_family Dom F.
An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF0 : set ⇒ intersection_of_family Dom F0) b0 Hb0FinInt).
Apply HexF to the current goal.
Let F be given.
Assume HFpair.
We prove the intermediate claim HFsub: F ∈ finite_subcollections S.
An exact proof term for the current goal is (andEL (F ∈ finite_subcollections S) (b0 = intersection_of_family Dom F) HFpair).
We prove the intermediate claim Hb0eq: b0 = intersection_of_family Dom F.
An exact proof term for the current goal is (andER (F ∈ finite_subcollections S) (b0 = intersection_of_family Dom F) HFpair).
rewrite the current goal using Hb0eq (from left to right).
Set F' to be the term {U ∩ CXY|U ∈ F}.
We prove the intermediate claim HFpowS: F ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 : set ⇒ finite F0) F HFsub).
We prove the intermediate claim HFinF: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 : set ⇒ finite F0) F HFsub).
We prove the intermediate claim HFinF': finite F'.
An exact proof term for the current goal is (Repl_finite (λU0 : set ⇒ U0 ∩ CXY) F HFinF).
We prove the intermediate claim HF'subTcc: F' ⊆ Tcc.
Let V be given.
Assume HV: V ∈ F'.
Apply (ReplE_impred F (λU0 : set ⇒ U0 ∩ CXY) V HV) to the current goal.
Let U0 be given.
Assume HU0F: U0 ∈ F.
Assume HVeq: V = U0 ∩ CXY.
We prove the intermediate claim HU0S: U0 ∈ S.
We prove the intermediate claim HFsubS: F ⊆ S.
An exact proof term for the current goal is (PowerE S F HFpowS).
An exact proof term for the current goal is (HFsubS U0 HU0F).
We prove the intermediate claim HexKU: ∃K U : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U ∈ Ty ∧ U0 = {f ∈ Dom|K ⊆ preimage_of X f U}.
An exact proof term for the current goal is (SepE2 (𝒫 Dom) (λS0 : set ⇒ ∃K U : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U ∈ Ty ∧ S0 = {f ∈ Dom|K ⊆ preimage_of X f U}) U0 HU0S).
Apply HexKU to the current goal.
Let K be given.
Assume HexU.
Apply HexU to the current goal.
Let U be given.
Assume HKUpack.
We prove the intermediate claim HKUAB: (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) ∧ U ∈ Ty.
An exact proof term for the current goal is (andEL ((compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) ∧ U ∈ Ty) (U0 = {f ∈ Dom|K ⊆ preimage_of X f U}) HKUpack).
We prove the intermediate claim HKU1: compact_space K (subspace_topology X Tx K) ∧ K ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) (U ∈ Ty) HKUAB).
We prove the intermediate claim HK: compact_space K (subspace_topology X Tx K).
An exact proof term for the current goal is (andEL (compact_space K (subspace_topology X Tx K)) (K ⊆ X) HKU1).
We prove the intermediate claim HKsubX: K ⊆ X.
An exact proof term for the current goal is (andER (compact_space K (subspace_topology X Tx K)) (K ⊆ X) HKU1).
We prove the intermediate claim HU: U ∈ Ty.
An exact proof term for the current goal is (andER (compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) (U ∈ Ty) HKUAB).
We prove the intermediate claim HU0eq2: U0 = {f ∈ Dom|K ⊆ preimage_of X f U}.
An exact proof term for the current goal is (andER ((compact_space K (subspace_topology X Tx K) ∧ K ⊆ X) ∧ U ∈ Ty) (U0 = {f ∈ Dom|K ⊆ preimage_of X f U}) HKUpack).
rewrite the current goal using HVeq (from left to right).
rewrite the current goal using HU0eq2 (from left to right).
We prove the intermediate claim HeqSset: ({f ∈ Dom|K ⊆ preimage_of X f U} ∩ CXY) = {f ∈ CXY|K ⊆ preimage_of X f U}.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ({f ∈ Dom|K ⊆ preimage_of X f U} ∩ CXY).
We will prove f ∈ {f ∈ CXY|K ⊆ preimage_of X f U}.
We prove the intermediate claim HfC: f ∈ CXY.
An exact proof term for the current goal is (binintersectE2 {f ∈ Dom|K ⊆ preimage_of X f U} CXY f Hf).
We prove the intermediate claim HfU0: f ∈ {f ∈ Dom|K ⊆ preimage_of X f U}.
An exact proof term for the current goal is (binintersectE1 {f ∈ Dom|K ⊆ preimage_of X f U} CXY f Hf).
We prove the intermediate claim HKpre: K ⊆ preimage_of X f U.
An exact proof term for the current goal is (SepE2 Dom (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f HfU0).
An exact proof term for the current goal is (SepI CXY (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f HfC HKpre).
Let f be given.
Assume Hf: f ∈ {f ∈ CXY|K ⊆ preimage_of X f U}.
We will prove f ∈ ({f ∈ Dom|K ⊆ preimage_of X f U} ∩ CXY).
We prove the intermediate claim HfC: f ∈ CXY.
An exact proof term for the current goal is (SepE1 CXY (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f Hf).
We prove the intermediate claim HfDom: f ∈ Dom.
An exact proof term for the current goal is (HCsub f HfC).
We prove the intermediate claim HKpre: K ⊆ preimage_of X f U.
An exact proof term for the current goal is (SepE2 CXY (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f Hf).
We prove the intermediate claim HfU0: f ∈ {f ∈ Dom|K ⊆ preimage_of X f U}.
An exact proof term for the current goal is (SepI Dom (λf0 : set ⇒ K ⊆ preimage_of X f0 U) f HfDom HKpre).
An exact proof term for the current goal is (binintersectI {f ∈ Dom|K ⊆ preimage_of X f U} CXY f HfU0 HfC).
rewrite the current goal using HeqSset (from left to right).
An exact proof term for the current goal is (compact_open_subbasic_C_open_in_compact_convergence_metric X Tx Y dY K U HTx HdY HK HKsubX HU).
We prove the intermediate claim HF'pow: F' ∈ 𝒫 Tcc.
An exact proof term for the current goal is (PowerI Tcc F' HF'subTcc).
We prove the intermediate claim Hinter: intersection_of_family CXY F' ∈ Tcc.
An exact proof term for the current goal is (finite_intersection_in_topology CXY Tcc F' HTcc HF'pow HFinF').
We prove the intermediate claim HeqInter: (intersection_of_family Dom F) ∩ CXY = intersection_of_family CXY F'.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ((intersection_of_family Dom F) ∩ CXY).
We will prove f ∈ intersection_of_family CXY F'.
We prove the intermediate claim HfC: f ∈ CXY.
An exact proof term for the current goal is (binintersectE2 (intersection_of_family Dom F) CXY f Hf).
Apply (intersection_of_familyI CXY F' f HfC) to the current goal.
Let V be given.
Assume HV: V ∈ F'.
We prove the intermediate claim HexU0: ∃U0 ∈ F, V = U0 ∩ CXY.
An exact proof term for the current goal is (ReplE F (λU0 : set ⇒ U0 ∩ CXY) V HV).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0F: U0 ∈ F.
An exact proof term for the current goal is (andEL (U0 ∈ F) (V = U0 ∩ CXY) HU0pair).
We prove the intermediate claim HVeq: V = U0 ∩ CXY.
An exact proof term for the current goal is (andER (U0 ∈ F) (V = U0 ∩ CXY) HU0pair).
rewrite the current goal using HVeq (from left to right).
We prove the intermediate claim HfInt: f ∈ intersection_of_family Dom F.
An exact proof term for the current goal is (binintersectE1 (intersection_of_family Dom F) CXY f Hf).
We prove the intermediate claim HfU0: f ∈ U0.
An exact proof term for the current goal is (intersection_of_familyE2 Dom F f HfInt U0 HU0F).
An exact proof term for the current goal is (binintersectI U0 CXY f HfU0 HfC).
Let f be given.
Assume Hf: f ∈ intersection_of_family CXY F'.
We will prove f ∈ ((intersection_of_family Dom F) ∩ CXY).
We prove the intermediate claim HfC: f ∈ CXY.
An exact proof term for the current goal is (intersection_of_familyE1 CXY F' f Hf).
We prove the intermediate claim HfIntDom: f ∈ intersection_of_family Dom F.
We prove the intermediate claim HfDom: f ∈ Dom.
An exact proof term for the current goal is (HCsub f HfC).
Apply (intersection_of_familyI Dom F f HfDom) to the current goal.
Let U0 be given.
Assume HU0F: U0 ∈ F.
We prove the intermediate claim HU0inF': (U0 ∩ CXY) ∈ F'.
An exact proof term for the current goal is (ReplI F (λU1 : set ⇒ U1 ∩ CXY) U0 HU0F).
We prove the intermediate claim HfInU0cap: f ∈ (U0 ∩ CXY).
An exact proof term for the current goal is (intersection_of_familyE2 CXY F' f Hf (U0 ∩ CXY) HU0inF').
An exact proof term for the current goal is (binintersectE1 U0 CXY f HfInU0cap).
An exact proof term for the current goal is (binintersectI (intersection_of_family Dom F) CXY f HfIntDom HfC).
rewrite the current goal using HeqInter (from left to right).
An exact proof term for the current goal is Hinter.
We prove the intermediate claim HgenSub: generated_topology CXY {b0 ∩ CXY|b0 ∈ B} ⊆ Tcc.
An exact proof term for the current goal is (generated_topology_finer_weak CXY {b0 ∩ CXY|b0 ∈ B} Tcc HTcc HgensInTcc).
Let U be given.
Assume HU: U ∈ Tco.
We will prove U ∈ Tcc.
We prove the intermediate claim HUgen: U ∈ generated_topology CXY {b0 ∩ CXY|b0 ∈ B}.
rewrite the current goal using HcoEq (from right to left).
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (HgenSub U HUgen).
∎