Let I, Xi and i be given.
Assume HcompTop: ∀j : set, j ∈ I → topology_on (space_family_set Xi j) (space_family_topology Xi j).
Assume HiI: i ∈ I.
Set X to be the term product_space I Xi.
Set Tx to be the term product_topology_full I Xi.
Set Y to be the term space_family_set Xi i.
Set Ty to be the term space_family_topology Xi i.
Set f to be the term product_eval_map I Xi i.
We prove the intermediate claim HIne: I ≠ Empty.
Assume HI0: I = Empty.
We prove the intermediate claim HiE: i ∈ Empty.
rewrite the current goal using HI0 (from right to left) at position 1.
An exact proof term for the current goal is HiI.
An exact proof term for the current goal is (EmptyE i HiE).
We prove the intermediate claim HSsub: subbasis_on X (product_subbasis_full I Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on I Xi HIne HcompTop).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (topology_from_subbasis_is_topology X (product_subbasis_full I Xi) HSsub).
We prove the intermediate claim Hfun: function_on f X Y.
Let g be given.
Assume HgX: g ∈ X.
We will prove apply_fun f g ∈ Y.
We prove the intermediate claim Hfg: apply_fun f g = apply_fun g i.
An exact proof term for the current goal is (apply_fun_graph X (λu : set ⇒ apply_fun u i) g HgX).
rewrite the current goal using Hfg (from left to right).
We prove the intermediate claim HgProp: total_function_on g I (space_family_union I Xi) ∧ functional_graph g ∧ ∀j : set, j ∈ I → apply_fun g j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod I (space_family_union I Xi))) (λg0 : set ⇒ total_function_on g0 I (space_family_union I Xi) ∧ functional_graph g0 ∧ ∀j : set, j ∈ I → apply_fun g0 j ∈ space_family_set Xi j) g HgX).
We prove the intermediate claim HgCoords: ∀j : set, j ∈ I → apply_fun g j ∈ space_family_set Xi j.
An exact proof term for the current goal is (andER (total_function_on g I (space_family_union I Xi) ∧ functional_graph g) (∀j : set, j ∈ I → apply_fun g j ∈ space_family_set Xi j) HgProp).
An exact proof term for the current goal is (HgCoords i HiI).
We will prove continuous_map X Tx Y Ty f.
We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y ∧ ∀U : set, U ∈ Ty → preimage_of X f U ∈ Tx.
Apply andI 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 HTx.
An exact proof term for the current goal is (HcompTop i HiI).
An exact proof term for the current goal is Hfun.
Let U be given.
Assume HU: U ∈ Ty.
We will prove preimage_of X f U ∈ Tx.
We prove the intermediate claim HcylEq: preimage_of X f U = product_cylinder I Xi i U.
Apply set_ext to the current goal.
Let g be given.
Assume HgPre: g ∈ preimage_of X f U.
We will prove g ∈ product_cylinder I Xi i U.
We prove the intermediate claim HgX: g ∈ X.
An exact proof term for the current goal is (SepE1 X (λu0 : set ⇒ apply_fun f u0 ∈ U) g HgPre).
We prove the intermediate claim HfgU: apply_fun f g ∈ U.
An exact proof term for the current goal is (SepE2 X (λu0 : set ⇒ apply_fun f u0 ∈ U) g HgPre).
We prove the intermediate claim Hfg: apply_fun f g = apply_fun g i.
An exact proof term for the current goal is (apply_fun_graph X (λu0 : set ⇒ apply_fun u0 i) g HgX).
We prove the intermediate claim HgiU: apply_fun g i ∈ U.
rewrite the current goal using Hfg (from right to left).
An exact proof term for the current goal is HfgU.
An exact proof term for the current goal is (SepI X (λu0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun u0 i ∈ U) g HgX (andI (i ∈ I ∧ U ∈ space_family_topology Xi i) (apply_fun g i ∈ U) (andI (i ∈ I) (U ∈ space_family_topology Xi i) HiI HU) HgiU)).
Let g be given.
Assume HgCyl: g ∈ product_cylinder I Xi i U.
We will prove g ∈ preimage_of X f U.
We prove the intermediate claim HgX: g ∈ X.
An exact proof term for the current goal is (SepE1 X (λu0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun u0 i ∈ U) g HgCyl).
We prove the intermediate claim HgProp: i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U.
An exact proof term for the current goal is (SepE2 X (λu0 : set ⇒ i ∈ I ∧ U ∈ space_family_topology Xi i ∧ apply_fun u0 i ∈ U) g HgCyl).
We prove the intermediate claim HgiU: apply_fun g i ∈ U.
An exact proof term for the current goal is (andER (i ∈ I ∧ U ∈ space_family_topology Xi i) (apply_fun g i ∈ U) HgProp).
We prove the intermediate claim Hpre_def: preimage_of X f U = {x0 ∈ X|apply_fun f x0 ∈ U}.
Use reflexivity.
rewrite the current goal using Hpre_def (from left to right) at position 1.
Apply (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U) g HgX) to the current goal.
We prove the intermediate claim Hfg: apply_fun f g = apply_fun g i.
An exact proof term for the current goal is (apply_fun_graph X (λu0 : set ⇒ apply_fun u0 i) g HgX).
rewrite the current goal using Hfg (from left to right).
An exact proof term for the current goal is HgiU.
rewrite the current goal using HcylEq (from left to right).
We prove the intermediate claim HcylSub: product_cylinder I Xi i U ∈ product_subbasis_full I Xi.
Set Fam to be the term (λj : set ⇒ {product_cylinder I Xi j V|V ∈ space_family_topology Xi j}).
We prove the intermediate claim HcylFam: product_cylinder I Xi i U ∈ Fam i.
An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λV0 : set ⇒ product_cylinder I Xi i V0) U HU).
An exact proof term for the current goal is (famunionI I Fam i (product_cylinder I Xi i U) HiI HcylFam).
An exact proof term for the current goal is (generated_topology_from_subbasis_contains_subbasis_elem X (product_subbasis_full I Xi) (product_cylinder I Xi i U) HSsub HcylSub).
∎