Let X, Tx, Y, Ty, Z, Tz and f be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HTz: topology_on Z Tz.
Assume Hcont: continuous_map (setprod X Z) (product_topology X Tx Z Tz) Y Ty f.
Set Dom to be the term function_space X Y.
Set Tdom to be the term compact_convergence_topology X Tx Y Ty.
Set CXY to be the term continuous_function_space X Tx Y Ty.
Set Tc to be the term compact_open_topology_C X Tx Y Ty.
Set idX to be the term {(x,x)|x ∈ X}.
We prove the intermediate claim HidX: continuous_map X Tx X Tx idX.
An exact proof term for the current goal is (identity_continuous X Tx HTx).
We prove the intermediate claim Hf_fun: function_on f (setprod X Z) Y.
An exact proof term for the current goal is (continuous_map_function_on (setprod X Z) (product_topology X Tx Z Tz) Y Ty f Hcont).
We prove the intermediate claim HTprod: topology_on (setprod X Z) (product_topology X Tx Z Tz).
An exact proof term for the current goal is (product_topology_is_topology X Tx Z Tz HTx HTz).
Set F to be the term graph Z (λz : set ⇒ compose_fun X (pair_map X idX (const_fun X z)) f).
We use F to witness the existential quantifier.
We prove the intermediate claim HF_fun: function_on F Z Dom.
Let z be given.
Assume HzZ: z ∈ Z.
rewrite the current goal using (apply_fun_graph Z (λz0 : set ⇒ compose_fun X (pair_map X idX (const_fun X z0)) f) z HzZ) (from left to right).
We prove the intermediate claim Hc: continuous_map X Tx Z Tz (const_fun X z).
An exact proof term for the current goal is (const_fun_continuous X Tx Z Tz z HTx HTz HzZ).
Set iz to be the term pair_map X idX (const_fun X z).
We prove the intermediate claim Hiz: continuous_map X Tx (setprod X Z) (product_topology X Tx Z Tz) iz.
An exact proof term for the current goal is (maps_into_products X Tx X Tx Z Tz idX (const_fun X z) HidX Hc).
We prove the intermediate claim Hiz_fun: function_on iz X (setprod X Z).
An exact proof term for the current goal is (continuous_map_function_on X Tx (setprod X Z) (product_topology X Tx Z Tz) iz Hiz).
An exact proof term for the current goal is (compose_fun_in_function_space X (setprod X Z) Y iz f Hiz_fun Hf_fun).
We prove the intermediate claim HSsub: subbasis_on Dom (compact_open_subbasis X Tx Y Ty).
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 HpreS: ∀S0 : set, S0 ∈ compact_open_subbasis X Tx Y Ty → preimage_of Z F S0 ∈ Tz.
Let S0 be given.
Assume HS0: S0 ∈ compact_open_subbasis X Tx Y Ty.
We prove the intermediate claim HS0prop: ∃K0 : set, ∃U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S0 = {g ∈ Dom|K0 ⊆ preimage_of X g U0}.
An exact proof term for the current goal is (SepE2 (𝒫 Dom) (λS : set ⇒ ∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S = {g ∈ Dom|K0 ⊆ preimage_of X g U0}) S0 HS0).
Apply HS0prop to the current goal.
Let K0 be given.
Assume HexU0: ∃U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S0 = {g ∈ Dom|K0 ⊆ preimage_of X g U0}.
Apply HexU0 to the current goal.
Let U0 be given.
Assume HKU0: compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S0 = {g ∈ Dom|K0 ⊆ preimage_of X g U0}.
We prove the intermediate claim HKU0abc: (compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) ∧ U0 ∈ Ty.
An exact proof term for the current goal is (andEL ((compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) ∧ U0 ∈ Ty) (S0 = {g ∈ Dom|K0 ⊆ preimage_of X g U0}) HKU0).
We prove the intermediate claim HK0ab: compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X.
An exact proof term for the current goal is (andEL (compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) (U0 ∈ Ty) HKU0abc).
We prove the intermediate claim HK0comp: compact_space K0 (subspace_topology X Tx K0).
An exact proof term for the current goal is (andEL (compact_space K0 (subspace_topology X Tx K0)) (K0 ⊆ X) HK0ab).
We prove the intermediate claim HK0subX: K0 ⊆ X.
An exact proof term for the current goal is (andER (compact_space K0 (subspace_topology X Tx K0)) (K0 ⊆ X) HK0ab).
We prove the intermediate claim HU0Ty: U0 ∈ Ty.
An exact proof term for the current goal is (andER (compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) (U0 ∈ Ty) HKU0abc).
We prove the intermediate claim HS0eq: S0 = {g ∈ Dom|K0 ⊆ preimage_of X g U0}.
An exact proof term for the current goal is (andER ((compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X) ∧ U0 ∈ Ty) (S0 = {g ∈ Dom|K0 ⊆ preimage_of X g U0}) HKU0).
Set P to be the term preimage_of Z F S0.
Set NFam to be the term {V ∈ Tz|V ⊆ P}.
We prove the intermediate claim HNFamSub: NFam ⊆ Tz.
Let V be given.
Assume HV: V ∈ NFam.
An exact proof term for the current goal is (SepE1 Tz (λV0 : set ⇒ V0 ⊆ P) V HV).
We prove the intermediate claim HPsubUnion: P ⊆ ⋃ NFam.
Let z0 be given.
Assume Hz0P: z0 ∈ P.
We will prove z0 ∈ ⋃ NFam.
We prove the intermediate claim Hz0Z: z0 ∈ Z.
An exact proof term for the current goal is (SepE1 Z (λz : set ⇒ apply_fun F z ∈ S0) z0 Hz0P).
We prove the intermediate claim HFz0S0: apply_fun F z0 ∈ S0.
An exact proof term for the current goal is (SepE2 Z (λz : set ⇒ apply_fun F z ∈ S0) z0 Hz0P).
We prove the intermediate claim HeqFz0: apply_fun F z0 = compose_fun X (pair_map X idX (const_fun X z0)) f.
rewrite the current goal using (apply_fun_graph Z (λz : set ⇒ compose_fun X (pair_map X idX (const_fun X z)) f) z0 Hz0Z) (from left to right).
Use reflexivity.
We prove the intermediate claim HFz0Dom: apply_fun F z0 ∈ Dom.
An exact proof term for the current goal is (HF_fun z0 Hz0Z).
We prove the intermediate claim HK0pre: K0 ⊆ preimage_of X (apply_fun F z0) U0.
We prove the intermediate claim HFz0S0': apply_fun F z0 ∈ {g ∈ Dom|K0 ⊆ preimage_of X g U0}.
rewrite the current goal using HS0eq (from right to left).
An exact proof term for the current goal is HFz0S0.
An exact proof term for the current goal is (SepE2 Dom (λg : set ⇒ K0 ⊆ preimage_of X g U0) (apply_fun F z0) HFz0S0').
Set N0 to be the term preimage_of (setprod X Z) f U0.
We prove the intermediate claim HN0Top: N0 ∈ product_topology X Tx Z Tz.
An exact proof term for the current goal is (continuous_map_preimage (setprod X Z) (product_topology X Tx Z Tz) Y Ty f Hcont U0 HU0Ty).
We prove the intermediate claim HK0z0sub: setprod K0 {z0} ⊆ N0.
Let p be given.
Assume Hp: p ∈ setprod K0 {z0}.
We will prove p ∈ N0.
We prove the intermediate claim Hp0: p 0 ∈ K0.
An exact proof term for the current goal is (ap0_Sigma K0 (λ_ : set ⇒ {z0}) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ {z0}.
An exact proof term for the current goal is (ap1_Sigma K0 (λ_ : set ⇒ {z0}) p Hp).
We prove the intermediate claim HpEta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta K0 {z0} p Hp).
We prove the intermediate claim Hp1eq: p 1 = z0.
An exact proof term for the current goal is (SingE z0 (p 1) Hp1).
rewrite the current goal using HpEta (from left to right).
rewrite the current goal using Hp1eq (from left to right).
We prove the intermediate claim Hp0pre: p 0 ∈ preimage_of X (apply_fun F z0) U0.
An exact proof term for the current goal is (HK0pre (p 0) Hp0).
We prove the intermediate claim Himg: apply_fun (apply_fun F z0) (p 0) ∈ U0.
An exact proof term for the current goal is (SepE2 X (λx : set ⇒ apply_fun (apply_fun F z0) x ∈ U0) (p 0) Hp0pre).
Set iz0 to be the term pair_map X idX (const_fun X z0).
We prove the intermediate claim Hp0X: p 0 ∈ X.
An exact proof term for the current goal is (HK0subX (p 0) Hp0).
We prove the intermediate claim Hiz0_fun: function_on iz0 X (setprod X Z).
We prove the intermediate claim Hc0: continuous_map X Tx Z Tz (const_fun X z0).
An exact proof term for the current goal is (const_fun_continuous X Tx Z Tz z0 HTx HTz Hz0Z).
We prove the intermediate claim Hiz0: continuous_map X Tx (setprod X Z) (product_topology X Tx Z Tz) iz0.
An exact proof term for the current goal is (maps_into_products X Tx X Tx Z Tz idX (const_fun X z0) HidX Hc0).
An exact proof term for the current goal is (continuous_map_function_on X Tx (setprod X Z) (product_topology X Tx Z Tz) iz0 Hiz0).
We prove the intermediate claim HcompVal: apply_fun (compose_fun X iz0 f) (p 0) = apply_fun f (apply_fun iz0 (p 0)).
An exact proof term for the current goal is (compose_fun_apply X iz0 f (p 0) Hp0X).
We prove the intermediate claim Hiz0Val: apply_fun iz0 (p 0) = (p 0,z0).
rewrite the current goal using (pair_map_apply X X Z idX (const_fun X z0) (p 0) Hp0X) (from left to right).
rewrite the current goal using (identity_function_apply X (p 0) Hp0X) (from left to right).
rewrite the current goal using (const_fun_apply X z0 (p 0) Hp0X) (from left to right).
Use reflexivity.
We prove the intermediate claim Himg1: apply_fun (compose_fun X iz0 f) (p 0) ∈ U0.
rewrite the current goal using HeqFz0 (from right to left).
An exact proof term for the current goal is Himg.
We prove the intermediate claim Himg2: apply_fun f (apply_fun iz0 (p 0)) ∈ U0.
rewrite the current goal using HcompVal (from right to left).
An exact proof term for the current goal is Himg1.
We prove the intermediate claim Himg3: apply_fun f (p 0,z0) ∈ U0.
rewrite the current goal using Hiz0Val (from right to left).
An exact proof term for the current goal is Himg2.
We prove the intermediate claim Hp0Z: z0 ∈ Z.
An exact proof term for the current goal is Hz0Z.
We prove the intermediate claim HpairXZ: (p 0,z0) ∈ setprod X Z.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Z (p 0) z0 Hp0X Hp0Z).
An exact proof term for the current goal is (SepI (setprod X Z) (λq : set ⇒ apply_fun f q ∈ U0) (p 0,z0) HpairXZ Himg3).
We prove the intermediate claim Htube: ∃V0 : set, V0 ∈ Tz ∧ z0 ∈ V0 ∧ setprod K0 V0 ⊆ N0.
An exact proof term for the current goal is (tube_lemma_compact_first X Tx Z Tz K0 HTx HTz HK0comp HK0subX z0 Hz0Z N0 (andI (N0 ∈ product_topology X Tx Z Tz) (setprod K0 {z0} ⊆ N0) HN0Top HK0z0sub)).
Apply Htube to the current goal.
Let V0 be given.
Assume HV0pack: V0 ∈ Tz ∧ z0 ∈ V0 ∧ setprod K0 V0 ⊆ N0.
We prove the intermediate claim HV0pair: V0 ∈ Tz ∧ z0 ∈ V0.
An exact proof term for the current goal is (andEL (V0 ∈ Tz ∧ z0 ∈ V0) (setprod K0 V0 ⊆ N0) HV0pack).
We prove the intermediate claim HV0Tz: V0 ∈ Tz.
An exact proof term for the current goal is (andEL (V0 ∈ Tz) (z0 ∈ V0) HV0pair).
We prove the intermediate claim Hz0V0: z0 ∈ V0.
An exact proof term for the current goal is (andER (V0 ∈ Tz) (z0 ∈ V0) HV0pair).
We prove the intermediate claim HK0V0sub: setprod K0 V0 ⊆ N0.
An exact proof term for the current goal is (andER (V0 ∈ Tz ∧ z0 ∈ V0) (setprod K0 V0 ⊆ N0) HV0pack).
We prove the intermediate claim HV0subP: V0 ⊆ P.
Let z1 be given.
Assume Hz1V0: z1 ∈ V0.
We will prove z1 ∈ P.
We will prove z1 ∈ preimage_of Z F S0.
We prove the intermediate claim Hz1Z: z1 ∈ Z.
An exact proof term for the current goal is (topology_elem_subset Z Tz V0 HTz HV0Tz z1 Hz1V0).
We prove the intermediate claim HFz1Dom: apply_fun F z1 ∈ Dom.
An exact proof term for the current goal is (HF_fun z1 Hz1Z).
We prove the intermediate claim HK0pre1: K0 ⊆ preimage_of X (apply_fun F z1) U0.
Let x be given.
Assume HxK0: x ∈ K0.
We will prove x ∈ preimage_of X (apply_fun F z1) U0.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HK0subX x HxK0).
We prove the intermediate claim HpairIn: (x,z1) ∈ setprod K0 V0.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K0 V0 x z1 HxK0 Hz1V0).
We prove the intermediate claim HxzN0: (x,z1) ∈ N0.
An exact proof term for the current goal is (HK0V0sub (x,z1) HpairIn).
We prove the intermediate claim HimgU0: apply_fun f (x,z1) ∈ U0.
An exact proof term for the current goal is (SepE2 (setprod X Z) (λq : set ⇒ apply_fun f q ∈ U0) (x,z1) HxzN0).
We prove the intermediate claim HeqFz1: apply_fun F z1 = compose_fun X (pair_map X idX (const_fun X z1)) f.
rewrite the current goal using (apply_fun_graph Z (λz : set ⇒ compose_fun X (pair_map X idX (const_fun X z)) f) z1 Hz1Z) (from left to right).
Use reflexivity.
Set iz1 to be the term pair_map X idX (const_fun X z1).
We prove the intermediate claim HvalEq: apply_fun (apply_fun F z1) x = apply_fun f (x,z1).
rewrite the current goal using HeqFz1 (from left to right).
rewrite the current goal using (compose_fun_apply X iz1 f x HxX) (from left to right).
rewrite the current goal using (pair_map_apply X X Z idX (const_fun X z1) x HxX) (from left to right).
rewrite the current goal using (identity_function_apply X x HxX) (from left to right).
rewrite the current goal using (const_fun_apply X z1 x HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim HvalU0: apply_fun (apply_fun F z1) x ∈ U0.
rewrite the current goal using HvalEq (from left to right).
An exact proof term for the current goal is HimgU0.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun (apply_fun F z1) u ∈ U0) x HxX HvalU0).
We prove the intermediate claim HFz1RHS: apply_fun F z1 ∈ {g ∈ Dom|K0 ⊆ preimage_of X g U0}.
An exact proof term for the current goal is (SepI Dom (λg : set ⇒ K0 ⊆ preimage_of X g U0) (apply_fun F z1) HFz1Dom HK0pre1).
We prove the intermediate claim HFz1S0: apply_fun F z1 ∈ S0.
rewrite the current goal using HS0eq (from left to right).
An exact proof term for the current goal is HFz1RHS.
An exact proof term for the current goal is (SepI Z (λz : set ⇒ apply_fun F z ∈ S0) z1 Hz1Z HFz1S0).
An exact proof term for the current goal is (UnionI NFam z0 V0 Hz0V0 (SepI Tz (λV : set ⇒ V ⊆ P) V0 HV0Tz HV0subP)).
We prove the intermediate claim HUnionSubP: ⋃ NFam ⊆ P.
Let z0 be given.
Assume Hz0U: z0 ∈ ⋃ NFam.
We will prove z0 ∈ P.
Apply (UnionE_impred NFam z0 Hz0U) to the current goal.
Let V0 be given.
Assume Hz0V0: z0 ∈ V0.
Assume HV0NF: V0 ∈ NFam.
We prove the intermediate claim HV0sub: V0 ⊆ P.
An exact proof term for the current goal is (SepE2 Tz (λV : set ⇒ V ⊆ P) V0 HV0NF).
An exact proof term for the current goal is (HV0sub z0 Hz0V0).
We prove the intermediate claim HPopen: P ∈ Tz.
We prove the intermediate claim HUnionIn: ⋃ NFam ∈ Tz.
An exact proof term for the current goal is (topology_union_closed Z Tz NFam HTz HNFamSub).
We prove the intermediate claim Heq: ⋃ NFam = P.
Apply set_ext to the current goal.
Let z0 be given.
Assume Hz0U: z0 ∈ ⋃ NFam.
An exact proof term for the current goal is (HUnionSubP z0 Hz0U).
Let z0 be given.
Assume Hz0P: z0 ∈ P.
An exact proof term for the current goal is (HPsubUnion z0 Hz0P).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HUnionIn.
An exact proof term for the current goal is HPopen.
We prove the intermediate claim HFdom: continuous_map Z Tz Dom Tdom F.
An exact proof term for the current goal is (continuous_map_from_subbasis Z Tz Dom (compact_open_subbasis X Tx Y Ty) F HTz HF_fun HSsub HpreS).
We prove the intermediate claim HimgCXY: ∀z : set, z ∈ Z → apply_fun F z ∈ CXY.
Let z be given.
Assume HzZ: z ∈ Z.
rewrite the current goal using (apply_fun_graph Z (λz0 : set ⇒ compose_fun X (pair_map X idX (const_fun X z0)) f) z HzZ) (from left to right).
We prove the intermediate claim Hc: continuous_map X Tx Z Tz (const_fun X z).
An exact proof term for the current goal is (const_fun_continuous X Tx Z Tz z HTx HTz HzZ).
Set iz to be the term pair_map X idX (const_fun X z).
We prove the intermediate claim Hiz: continuous_map X Tx (setprod X Z) (product_topology X Tx Z Tz) iz.
An exact proof term for the current goal is (maps_into_products X Tx X Tx Z Tz idX (const_fun X z) HidX Hc).
We prove the intermediate claim Hgz: continuous_map X Tx Y Ty (compose_fun X iz f).
An exact proof term for the current goal is (composition_continuous X Tx (setprod X Z) (product_topology X Tx Z Tz) Y Ty iz f Hiz Hcont).
We prove the intermediate claim Hiz_fun: function_on iz X (setprod X Z).
An exact proof term for the current goal is (continuous_map_function_on X Tx (setprod X Z) (product_topology X Tx Z Tz) iz Hiz).
We prove the intermediate claim HgzDom: compose_fun X iz f ∈ Dom.
An exact proof term for the current goal is (compose_fun_in_function_space X (setprod X Z) Y iz f Hiz_fun Hf_fun).
An exact proof term for the current goal is (SepI Dom (λg : set ⇒ continuous_map X Tx Y Ty g) (compose_fun X iz f) HgzDom Hgz).
An exact proof term for the current goal is (continuous_map_range_restrict Z Tz Dom Tdom F CXY HFdom (continuous_function_space_sub X Tx Y Ty) HimgCXY).
∎