Let A, Ta, X, Tx, Y, Ty, f and g be given.
Assume Hf: continuous_map A Ta X Tx f.
Assume Hg: continuous_map A Ta Y Ty g.
We prove the intermediate claim Hf_mid: (topology_on A Ta ∧ topology_on X Tx) ∧ function_on f A X.
An exact proof term for the current goal is (andEL ((topology_on A Ta ∧ topology_on X Tx) ∧ function_on f A X) (∀V : set, V ∈ Tx → preimage_of A f V ∈ Ta) Hf).
We prove the intermediate claim Hfun_f: function_on f A X.
An exact proof term for the current goal is (andER (topology_on A Ta ∧ topology_on X Tx) (function_on f A X) Hf_mid).
We prove the intermediate claim HtopAX: 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 f A X) Hf_mid).
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) HtopAX).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andER (topology_on A Ta) (topology_on X Tx) HtopAX).
We prove the intermediate claim Hf_pre: ∀U : set, U ∈ Tx → preimage_of A f U ∈ Ta.
An exact proof term for the current goal is (andER ((topology_on A Ta ∧ topology_on X Tx) ∧ function_on f A X) (∀V : set, V ∈ Tx → preimage_of A f V ∈ Ta) Hf).
We prove the intermediate claim Hg_mid: (topology_on A Ta ∧ topology_on Y Ty) ∧ function_on g A Y.
An exact proof term for the current goal is (andEL ((topology_on A Ta ∧ topology_on Y Ty) ∧ function_on g A Y) (∀V : set, V ∈ Ty → preimage_of A g V ∈ Ta) Hg).
We prove the intermediate claim Hfun_g: function_on g A Y.
An exact proof term for the current goal is (andER (topology_on A Ta ∧ topology_on Y Ty) (function_on g A Y) Hg_mid).
We prove the intermediate claim HtopAY: topology_on A Ta ∧ topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on A Ta ∧ topology_on Y Ty) (function_on g A Y) Hg_mid).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andER (topology_on A Ta) (topology_on Y Ty) HtopAY).
We prove the intermediate claim Hg_pre: ∀V : set, V ∈ Ty → preimage_of A g V ∈ Ta.
An exact proof term for the current goal is (andER ((topology_on A Ta ∧ topology_on Y Ty) ∧ function_on g A Y) (∀V : set, V ∈ Ty → preimage_of A g V ∈ Ta) Hg).
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 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 will prove continuous_map A Ta (setprod X Y) (product_topology X Tx Y Ty) (pair_map A f g).
We will prove topology_on A Ta ∧ topology_on (setprod X Y) (product_topology X Tx Y Ty) ∧ function_on (pair_map A f g) A (setprod X Y) ∧ ∀W : set, W ∈ product_topology X Tx Y Ty → preimage_of A (pair_map A f g) 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.
Let a be given.
Assume HaA: a ∈ A.
We will prove apply_fun (pair_map A f g) a ∈ setprod X Y.
We prove the intermediate claim Happ: apply_fun (pair_map A f g) a = (apply_fun f a,apply_fun g a).
An exact proof term for the current goal is (pair_map_apply A X Y f g a HaA).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Y (apply_fun f a) (apply_fun g a) (Hfun_f a HaA) (Hfun_g a HaA)).
Let W be given.
Assume HW: W ∈ product_topology X Tx Y Ty.
We will prove preimage_of A (pair_map A f g) W ∈ Ta.
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 (pair_map A f g) b|b ∈ Fam}.
We prove the intermediate claim HpreEq1: preimage_of A (pair_map A f g) W = preimage_of A (pair_map A f g) (⋃ Fam).
rewrite the current goal using HUnionEq (from right to left).
Use reflexivity.
We prove the intermediate claim HpreEq2: preimage_of A (pair_map A f g) (⋃ Fam) = ⋃ PreFam.
rewrite the current goal using (preimage_of_Union A (pair_map A f g) Fam) (from left to right).
Use reflexivity.
rewrite the current goal using HpreEq1 (from left to right).
rewrite the current goal using HpreEq2 (from left to right).
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 (pair_map A f g) b) P HP) to the current goal.
Let b be given.
Assume HbFam: b ∈ Fam.
Assume HPeq: P = preimage_of A (pair_map A f g) b.
We prove the intermediate claim HbSub: b ∈ product_subbasis X Tx Y Ty.
An exact proof term for the current goal is (HFamSub b HbFam).
We prove the intermediate claim HexU: ∃U ∈ Tx, b ∈ {rectangle_set U V|V ∈ Ty}.
An exact proof term for the current goal is (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbSub).
Apply HexU to the current goal.
Let U be given.
Assume HUconj: U ∈ Tx ∧ b ∈ {rectangle_set U V|V ∈ Ty}.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (b ∈ {rectangle_set U V|V ∈ Ty}) HUconj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U V|V ∈ Ty}.
An exact proof term for the current goal is (andER (U ∈ Tx) (b ∈ {rectangle_set U V|V ∈ 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 HV: 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 HpreRect: preimage_of A (pair_map A f g) b = (preimage_of A f U) ∩ (preimage_of A g V).
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (preimage_pair_map_rectangle A X Y f g U V).
rewrite the current goal using HPeq (from left to right).
rewrite the current goal using HpreRect (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed A Ta (preimage_of A f U) (preimage_of A g V) HTa (Hf_pre U HU) (Hg_pre V HV)).
We prove the intermediate claim HPreFamPow: PreFam ∈ 𝒫 Ta.
Apply PowerI to the current goal.
An exact proof term for the current goal is HPreFamSub.
An exact proof term for the current goal is (topology_union_axiom A Ta HTa PreFam HPreFamPow).
∎