Let A, Ta, X, Tx, Y, Ty and h be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume Hfunh: function_on h A (setprod X Y).
Assume Hc1: continuous_map A Ta X Tx (compose_fun A h (projection_map1 X Y)).
Assume Hc2: continuous_map A Ta Y Ty (compose_fun A h (projection_map2 X Y)).
We will prove continuous_map A Ta (setprod X Y) (product_topology X Tx Y Ty) h.
Set h1 to be the term compose_fun A h (projection_map1 X Y).
Set h2 to be the term compose_fun A h (projection_map2 X Y).
We prove the intermediate claim Hc1_left: (topology_on A Ta ∧ topology_on X Tx) ∧ function_on h1 A X.
An exact proof term for the current goal is (andEL ((topology_on A Ta ∧ topology_on X Tx) ∧ function_on h1 A X) (∀U : set, U ∈ Tx → preimage_of A h1 U ∈ Ta) Hc1).
We prove the intermediate claim HTaX: topology_on A Ta ∧ topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on A Ta ∧ topology_on X Tx) (function_on h1 A X) Hc1_left).
We prove the intermediate claim HTa: topology_on A Ta.
An exact proof term for the current goal is (andEL (topology_on A Ta) (topology_on X Tx) HTaX).
We prove the intermediate claim Hpre1: ∀U : set, U ∈ Tx → preimage_of A h1 U ∈ Ta.
An exact proof term for the current goal is (andER ((topology_on A Ta ∧ topology_on X Tx) ∧ function_on h1 A X) (∀U : set, U ∈ Tx → preimage_of A h1 U ∈ Ta) Hc1).
We prove the intermediate claim Hc2_left: (topology_on A Ta ∧ topology_on Y Ty) ∧ function_on h2 A Y.
An exact proof term for the current goal is (andEL ((topology_on A Ta ∧ topology_on Y Ty) ∧ function_on h2 A Y) (∀V : set, V ∈ Ty → preimage_of A h2 V ∈ Ta) Hc2).
We prove the intermediate claim Hpre2: ∀V : set, V ∈ Ty → preimage_of A h2 V ∈ Ta.
An exact proof term for the current goal is (andER ((topology_on A Ta ∧ topology_on Y Ty) ∧ function_on h2 A Y) (∀V : set, V ∈ Ty → preimage_of A h2 V ∈ Ta) Hc2).
We prove the intermediate claim HTprod: topology_on (setprod X Y) (product_topology X Tx Y Ty).
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We will prove ((topology_on A Ta ∧ topology_on (setprod X Y) (product_topology X Tx Y Ty)) ∧ function_on h A (setprod X Y)) ∧ (∀W : set, W ∈ product_topology X Tx Y Ty → preimage_of A h W ∈ Ta).
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 HTa.
An exact proof term for the current goal is HTprod.
An exact proof term for the current goal is Hfunh.
Let W be given.
Assume HW: W ∈ product_topology X Tx Y Ty.
We will prove preimage_of A h W ∈ Ta.
We prove the intermediate claim HBasis: basis_on (setprod X Y) (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim HWopen: open_in (setprod X Y) (product_topology X Tx Y Ty) W.
An exact proof term for the current goal is (andI (topology_on (setprod X Y) (product_topology X Tx Y Ty)) (W ∈ product_topology X Tx Y Ty) HTprod HW).
Apply (open_sets_as_unions_of_basis (setprod X Y) (product_subbasis X Tx Y Ty) HBasis W HWopen) to the current goal.
Let Fam be given.
Assume HFamPair.
We prove the intermediate claim HFamPow: Fam ∈ 𝒫 (product_subbasis X Tx Y Ty).
An exact proof term for the current goal is (andEL (Fam ∈ 𝒫 (product_subbasis X Tx Y Ty)) (⋃ Fam = W) HFamPair).
We prove the intermediate claim HUnionEq: ⋃ Fam = W.
An exact proof term for the current goal is (andER (Fam ∈ 𝒫 (product_subbasis X Tx Y Ty)) (⋃ Fam = W) HFamPair).
We prove the intermediate claim HFamSub: Fam ⊆ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (PowerE (product_subbasis X Tx Y Ty) Fam HFamPow).
Set PreFam to be the term {preimage_of A h b|b ∈ Fam}.
We prove the intermediate claim HpreEq1: preimage_of A h W = preimage_of A h (⋃ Fam).
rewrite the current goal using HUnionEq (from right to left).
Use reflexivity.
We prove the intermediate claim HpreEq2: preimage_of A h (⋃ Fam) = ⋃ PreFam.
rewrite the current goal using (preimage_of_Union A h Fam) (from left to right).
Use reflexivity.
We prove the intermediate claim HPreFamSub: PreFam ⊆ Ta.
Let P be given.
Assume HP: P ∈ PreFam.
Apply (ReplE_impred Fam (λb : set ⇒ preimage_of A h b) P HP (P ∈ Ta)) to the current goal.
Let b be given.
Assume HbFam: b ∈ Fam.
Assume HPeq: P = preimage_of A h b.
We prove the intermediate claim HbB: b ∈ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (HFamSub b HbFam).
Apply (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) b HbB) to the current goal.
Let U be given.
Assume HUconj: U ∈ Tx ∧ b ∈ {rectangle_set U V0|V0 ∈ Ty}.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (b ∈ {rectangle_set U V0|V0 ∈ Ty}) HUconj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U V0|V0 ∈ Ty}.
An exact proof term for the current goal is (andER (U ∈ Tx) (b ∈ {rectangle_set U V0|V0 ∈ Ty}) HUconj).
We prove the intermediate claim HexV: ∃V ∈ Ty, b = rectangle_set U V.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U V0) b HbRepl).
Apply HexV to the current goal.
Let V be given.
Assume HVconj: V ∈ Ty ∧ b = rectangle_set U V.
We prove the intermediate claim HVinTy: V ∈ Ty.
An exact proof term for the current goal is (andEL (V ∈ Ty) (b = rectangle_set U V) HVconj).
We prove the intermediate claim Hbeq: b = rectangle_set U V.
An exact proof term for the current goal is (andER (V ∈ Ty) (b = rectangle_set U V) HVconj).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HVsubY: V ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y Ty V HTy HVinTy).
We prove the intermediate claim HpreRect: preimage_of A h (rectangle_set U V) = (preimage_of A h1 U) ∩ (preimage_of A h2 V).
An exact proof term for the current goal is (preimage_of_rectangle_via_projections A X Y h U V Hfunh HUsubX HVsubY).
We prove the intermediate claim HpreU: preimage_of A h1 U ∈ Ta.
An exact proof term for the current goal is (Hpre1 U HUinTx).
We prove the intermediate claim HpreV: preimage_of A h2 V ∈ Ta.
An exact proof term for the current goal is (Hpre2 V HVinTy).
We prove the intermediate claim Hcap: (preimage_of A h1 U) ∩ (preimage_of A h2 V) ∈ Ta.
An exact proof term for the current goal is (topology_binintersect_closed A Ta (preimage_of A h1 U) (preimage_of A h2 V) HTa HpreU HpreV).
We prove the intermediate claim HpreB: preimage_of A h b ∈ Ta.
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using HpreRect (from left to right).
An exact proof term for the current goal is Hcap.
rewrite the current goal using HPeq (from left to right).
An exact proof term for the current goal is HpreB.
We prove the intermediate claim HPreFamPow: PreFam ∈ 𝒫 Ta.
Apply PowerI to the current goal.
An exact proof term for the current goal is HPreFamSub.
We prove the intermediate claim HUnionPre: ⋃ PreFam ∈ Ta.
An exact proof term for the current goal is (topology_union_axiom A Ta HTa PreFam HPreFamPow).
rewrite the current goal using HpreEq1 (from left to right).
rewrite the current goal using HpreEq2 (from left to right).
An exact proof term for the current goal is HUnionPre.
∎