Let X, Tx, F and J be given.
Assume HTx: topology_on X Tx.
Assume HJne: J ≠ Empty.
Assume Htot: total_function_on F J (function_space X unit_interval).
Assume HcontCoord: ∀j : set, j ∈ J → continuous_map X Tx unit_interval unit_interval_topology (apply_fun F j).
Set Xi to be the term const_space_family J unit_interval unit_interval_topology.
Set Ty to be the term product_topology_full J Xi.
We will prove continuous_map X Tx (unit_interval_power J) Ty (diagonal_map X F J).
We prove the intermediate claim HYdef: unit_interval_power J = product_space J Xi.
Use reflexivity.
We prove the intermediate claim Hfun: function_on (diagonal_map X F J) X (unit_interval_power J).
An exact proof term for the current goal is (diagonal_map_function_on_unit_interval_power X F J Htot).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ J → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiJ: i ∈ J.
rewrite the current goal using (space_family_set_const_space_family J unit_interval unit_interval_topology i HiJ) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family J unit_interval unit_interval_topology i HiJ) (from left to right).
An exact proof term for the current goal is unit_interval_topology_on.
We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HJne HcompTop).
We prove the intermediate claim HfunY: function_on (diagonal_map X F J) X (product_space J Xi).
rewrite the current goal using HYdef (from right to left).
An exact proof term for the current goal is Hfun.
rewrite the current goal using HYdef (from left to right).
Apply (continuous_map_from_subbasis X Tx (product_space J Xi) (product_subbasis_full J Xi) (diagonal_map X F J) HTx HfunY HSsub) to the current goal.
Let s be given.
Assume HsS: s ∈ product_subbasis_full J Xi.
We will prove preimage_of X (diagonal_map X F J) s ∈ Tx.
Set Fam to be the term (λi0 : set ⇒ {product_cylinder J Xi i0 U0|U0 ∈ space_family_topology Xi i0}).
We prove the intermediate claim HsFam: s ∈ (⋃i0 ∈ JFam i0).
An exact proof term for the current goal is HsS.
Apply (famunionE_impred J Fam s HsFam (preimage_of X (diagonal_map X F J) s ∈ Tx)) to the current goal.
Let i be given.
Assume HiJ: i ∈ J.
Assume HsFi: s ∈ Fam i.
We prove the intermediate claim HexU: ∃U ∈ space_family_topology Xi i, s = product_cylinder J Xi i U.
An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder J Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U be given.
Assume HUand: U ∈ space_family_topology Xi i ∧ s = product_cylinder J Xi i U.
We prove the intermediate claim HUtop: U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (U ∈ space_family_topology Xi i) (s = product_cylinder J Xi i U) HUand).
We prove the intermediate claim Hseq: s = product_cylinder J Xi i U.
An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (s = product_cylinder J Xi i U) HUand).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Hconti: continuous_map X Tx unit_interval unit_interval_topology (apply_fun F i).
An exact proof term for the current goal is (HcontCoord i HiJ).
We prove the intermediate claim HUui: U ∈ unit_interval_topology.
We prove the intermediate claim Htopi: space_family_topology Xi i = unit_interval_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J unit_interval unit_interval_topology i HiJ).
rewrite the current goal using Htopi (from right to left).
An exact proof term for the current goal is HUtop.
We prove the intermediate claim HpreEq: preimage_of X (diagonal_map X F J) (product_cylinder J Xi i U) = preimage_of X (apply_fun F i) U.
Apply set_ext to the current goal.
Let x be given.
Assume HxPre: x ∈ preimage_of X (diagonal_map X F J) (product_cylinder J Xi i U).
We will prove x ∈ preimage_of X (apply_fun F i) U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (diagonal_map X F J) x0 ∈ product_cylinder J Xi i U) x HxPre).
We prove the intermediate claim HfxCyl: apply_fun (diagonal_map X F J) x ∈ product_cylinder J Xi i U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (diagonal_map X F J) x0 ∈ product_cylinder J Xi i U) x HxPre).
We prove the intermediate claim HcylProp: i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun (diagonal_map X F J) x) i ∈ U.
An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf0 : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) (apply_fun (diagonal_map X F J) x) HfxCyl).
We prove the intermediate claim HcoordU: apply_fun (apply_fun (diagonal_map X F J) x) i ∈ U.
We prove the intermediate claim H12: i ∈ J ∧ U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun (diagonal_map X F J) x) i ∈ U) HcylProp).
An exact proof term for the current goal is (andER (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun (diagonal_map X F J) x) i ∈ U) HcylProp).
We prove the intermediate claim HFmapx: apply_fun (diagonal_map X F J) x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun (diagonal_map X F J) x) i = apply_fun (apply_fun F i) x.
rewrite the current goal using HFmapx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HfiU: apply_fun (apply_fun F i) x ∈ U.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is HcoordU.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxX HfiU).
Let x be given.
Assume HxPre: x ∈ preimage_of X (apply_fun F i) U.
We will prove x ∈ preimage_of X (diagonal_map X F J) (product_cylinder J Xi i U).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxPre).
We prove the intermediate claim HfiU: apply_fun (apply_fun F i) x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxPre).
We prove the intermediate claim HFmapx: apply_fun (diagonal_map X F J) x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun (diagonal_map X F J) x) i = apply_fun (apply_fun F i) x.
rewrite the current goal using HFmapx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HcoordU: apply_fun (apply_fun (diagonal_map X F J) x) i ∈ U.
rewrite the current goal using HcoordEq (from left to right).
An exact proof term for the current goal is HfiU.
We prove the intermediate claim HfunPow0: function_on (diagonal_map X F J) X (unit_interval_power J).
An exact proof term for the current goal is (diagonal_map_function_on_unit_interval_power X F J Htot).
We prove the intermediate claim HfunPow: function_on (diagonal_map X F J) X (product_space J Xi).
rewrite the current goal using HYdef (from right to left).
An exact proof term for the current goal is HfunPow0.
We prove the intermediate claim HfxY: apply_fun (diagonal_map X F J) x ∈ product_space J Xi.
An exact proof term for the current goal is (HfunPow x HxX).
We prove the intermediate claim HfxCyl: apply_fun (diagonal_map X F J) x ∈ product_cylinder J Xi i U.
We prove the intermediate claim HcylDef: product_cylinder J Xi i U = {f0 ∈ product_space J Xi|i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U}.
Use reflexivity.
rewrite the current goal using HcylDef (from left to right).
Apply (SepI (product_space J Xi) (λf0 : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) (apply_fun (diagonal_map X F J) x) HfxY) 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 HiJ.
An exact proof term for the current goal is HUtop.
An exact proof term for the current goal is HcoordU.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (diagonal_map X F J) x0 ∈ product_cylinder J Xi i U) x HxX HfxCyl).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage X Tx unit_interval unit_interval_topology (apply_fun F i) Hconti U HUui).
∎