Let X, Tx, Y and Ty be given.
Assume HX: connected_space X Tx.
Assume HY: connected_space Y Ty.
We will prove connected_space (setprod X Y) (product_topology X Tx Y Ty).
We prove the intermediate claim Hsetprod_empty_left: ∀Y0 : set, setprod Empty Y0 = Empty.
Let Y0 be given.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ setprod Empty Y0.
We will prove p ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim Hp0: (p 0) ∈ Empty.
An exact proof term for the current goal is (ap0_Sigma Empty (λ_ : set ⇒ Y0) p Hp).
An exact proof term for the current goal is (EmptyE (p 0) Hp0).
Let p be given.
Assume Hp: p ∈ Empty.
We will prove p ∈ setprod Empty Y0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE p Hp).
We prove the intermediate claim Hsetprod_empty_right: ∀X0 : set, setprod X0 Empty = Empty.
Let X0 be given.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ setprod X0 Empty.
We will prove p ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim Hp1: (p 1) ∈ Empty.
An exact proof term for the current goal is (ap1_Sigma X0 (λ_ : set ⇒ Empty) p Hp).
An exact proof term for the current goal is (EmptyE (p 1) Hp1).
Let p be given.
Assume Hp: p ∈ Empty.
We will prove p ∈ setprod X0 Empty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE p Hp).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (¬ (∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ separation_of X U V)) HX).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on Y Ty) (¬ (∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ separation_of Y U V)) HY).
Apply xm (X = Empty) to the current goal.
Assume HXEmpty: X = Empty.
rewrite the current goal using HXEmpty (from left to right).
rewrite the current goal using (Hsetprod_empty_left Y) (from left to right).
We will prove topology_on Empty (product_topology Empty Tx Y Ty) ∧ ¬ (∃U V : set, U ∈ product_topology Empty Tx Y Ty ∧ V ∈ product_topology Empty Tx Y Ty ∧ separation_of Empty U V).
Apply andI to the current goal.
We prove the intermediate claim HTx0: topology_on Empty Tx.
rewrite the current goal using HXEmpty (from right to left).
An exact proof term for the current goal is HTx.
We will prove topology_on Empty (product_topology Empty Tx Y Ty).
rewrite the current goal using (Hsetprod_empty_left Y) (from right to left) at position 1.
An exact proof term for the current goal is (product_topology_is_topology Empty Tx Y Ty HTx0 HTy).
We will prove ¬ (∃U V : set, U ∈ product_topology Empty Tx Y Ty ∧ V ∈ product_topology Empty Tx Y Ty ∧ separation_of Empty U V).
Assume Hsep: ∃U V : set, U ∈ product_topology Empty Tx Y Ty ∧ V ∈ product_topology Empty Tx Y Ty ∧ separation_of Empty U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ product_topology Empty Tx Y Ty ∧ V ∈ product_topology Empty Tx Y Ty ∧ separation_of Empty U V.
Apply HexV to the current goal.
Let V be given.
Assume HUVsep.
We prove the intermediate claim HsepUV: separation_of Empty U V.
An exact proof term for the current goal is (andER (U ∈ product_topology Empty Tx Y Ty ∧ V ∈ product_topology Empty Tx Y Ty) (separation_of Empty U V) HUVsep).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = Empty) HsepUV).
We prove the intermediate claim Hpart2: ((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty.
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) (U ≠ Empty) Hpart2).
We prove the intermediate claim Hpow: (U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) (U ≠ Empty) Hpart2).
We prove the intermediate claim HpowUV: U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) (U ∩ V = Empty) Hpow).
We prove the intermediate claim HUsub: U ⊆ Empty.
An exact proof term for the current goal is (PowerE Empty U (andEL (U ∈ 𝒫 Empty) (V ∈ 𝒫 Empty) HpowUV)).
We prove the intermediate claim HUeq: U = Empty.
An exact proof term for the current goal is (Empty_Subq_eq U HUsub).
An exact proof term for the current goal is (HUne HUeq).
Assume HXNonEmpty: X ≠ Empty.
Apply xm (Y = Empty) to the current goal.
Assume HYEmpty: Y = Empty.
rewrite the current goal using HYEmpty (from left to right).
rewrite the current goal using (Hsetprod_empty_right X) (from left to right).
We will prove topology_on Empty (product_topology X Tx Empty Ty) ∧ ¬ (∃U V : set, U ∈ product_topology X Tx Empty Ty ∧ V ∈ product_topology X Tx Empty Ty ∧ separation_of Empty U V).
Apply andI to the current goal.
We prove the intermediate claim HTy0: topology_on Empty Ty.
rewrite the current goal using HYEmpty (from right to left).
An exact proof term for the current goal is HTy.
We will prove topology_on Empty (product_topology X Tx Empty Ty).
rewrite the current goal using (Hsetprod_empty_right X) (from right to left) at position 1.
An exact proof term for the current goal is (product_topology_is_topology X Tx Empty Ty HTx HTy0).
We will prove ¬ (∃U V : set, U ∈ product_topology X Tx Empty Ty ∧ V ∈ product_topology X Tx Empty Ty ∧ separation_of Empty U V).
Assume Hsep: ∃U V : set, U ∈ product_topology X Tx Empty Ty ∧ V ∈ product_topology X Tx Empty Ty ∧ separation_of Empty U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ product_topology X Tx Empty Ty ∧ V ∈ product_topology X Tx Empty Ty ∧ separation_of Empty U V.
Apply HexV to the current goal.
Let V be given.
Assume HUVsep.
We prove the intermediate claim HsepUV: separation_of Empty U V.
An exact proof term for the current goal is (andER (U ∈ product_topology X Tx Empty Ty ∧ V ∈ product_topology X Tx Empty Ty) (separation_of Empty U V) HUVsep).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = Empty) HsepUV).
We prove the intermediate claim Hpart2: ((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty.
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) (U ≠ Empty) Hpart2).
We prove the intermediate claim Hpow: (U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) ∧ U ∩ V = Empty) (U ≠ Empty) Hpart2).
We prove the intermediate claim HpowUV: U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 Empty ∧ V ∈ 𝒫 Empty) (U ∩ V = Empty) Hpow).
We prove the intermediate claim HUsub: U ⊆ Empty.
An exact proof term for the current goal is (PowerE Empty U (andEL (U ∈ 𝒫 Empty) (V ∈ 𝒫 Empty) HpowUV)).
We prove the intermediate claim HUeq: U = Empty.
An exact proof term for the current goal is (Empty_Subq_eq U HUsub).
An exact proof term for the current goal is (HUne HUeq).
Assume HYNonEmpty: Y ≠ Empty.
Apply (nonempty_has_element X HXNonEmpty) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Apply (nonempty_has_element Y HYNonEmpty) to the current goal.
Let y0 be given.
Assume Hy0Y: y0 ∈ Y.
Set Top to be the term product_topology X Tx Y Ty.
Set Hhor to be the term setprod X {y0}.
Set F to be the term {setprod {x} Y ∪ Hhor|x ∈ X}.
We prove the intermediate claim HTprod: topology_on (setprod X Y) Top.
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HFsub: ∀C : set, C ∈ F → C ⊆ setprod X Y.
Let C be given.
Assume HC: C ∈ F.
Apply (ReplE_impred X (λx : set ⇒ setprod {x} Y ∪ Hhor) C HC) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume HCeq: C = setprod {x} Y ∪ Hhor.
rewrite the current goal using HCeq (from left to right).
We will prove (setprod {x} Y ∪ Hhor) ⊆ setprod X Y.
Let p be given.
Assume Hp: p ∈ setprod {x} Y ∪ Hhor.
We will prove p ∈ setprod X Y.
Apply (binunionE' (setprod {x} Y) Hhor p (p ∈ setprod X Y)) to the current goal.
Assume HpA: p ∈ setprod {x} Y.
We prove the intermediate claim Hxsub: {x} ⊆ X.
An exact proof term for the current goal is (singleton_subset x X HxX).
We prove the intermediate claim HYsub: Y ⊆ Y.
An exact proof term for the current goal is (Subq_ref Y).
An exact proof term for the current goal is (setprod_Subq {x} Y X Y Hxsub HYsub p HpA).
Assume HpB: p ∈ Hhor.
We prove the intermediate claim HXsub: X ⊆ X.
An exact proof term for the current goal is (Subq_ref X).
We prove the intermediate claim Hy0sub: {y0} ⊆ Y.
An exact proof term for the current goal is (singleton_subset y0 Y Hy0Y).
An exact proof term for the current goal is (setprod_Subq X {y0} X Y HXsub Hy0sub p HpB).
An exact proof term for the current goal is Hp.
We prove the intermediate claim HFconn: ∀C : set, C ∈ F → connected_space C (subspace_topology (setprod X Y) Top C).
Let C be given.
Assume HC: C ∈ F.
Apply (ReplE_impred X (λx : set ⇒ setprod {x} Y ∪ Hhor) C HC) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume HCeq: C = setprod {x} Y ∪ Hhor.
rewrite the current goal using HCeq (from left to right).
Set A to be the term setprod {x} Y.
Set B to be the term Hhor.
We prove the intermediate claim HAconn: connected_space A (subspace_topology (setprod X Y) Top A).
An exact proof term for the current goal is (slice_Y_connected X Tx Y Ty x HY HTx HxX).
We prove the intermediate claim HBconn: connected_space B (subspace_topology (setprod X Y) Top B).
An exact proof term for the current goal is (slice_X_connected X Tx Y Ty y0 HX HTy Hy0Y).
We prove the intermediate claim HABsub: ∀D : set, D ∈ {A,B} → D ⊆ setprod X Y.
Let D be given.
Assume HD: D ∈ {A,B}.
Apply (UPairE D A B HD (D ⊆ setprod X Y)) to the current goal.
Assume HDa: D = A.
rewrite the current goal using HDa (from left to right).
We prove the intermediate claim Hxsub: {x} ⊆ X.
An exact proof term for the current goal is (singleton_subset x X HxX).
We prove the intermediate claim HYsub: Y ⊆ Y.
An exact proof term for the current goal is (Subq_ref Y).
An exact proof term for the current goal is (setprod_Subq {x} Y X Y Hxsub HYsub).
Assume HDb: D = B.
rewrite the current goal using HDb (from left to right).
We prove the intermediate claim HXsub: X ⊆ X.
An exact proof term for the current goal is (Subq_ref X).
We prove the intermediate claim Hy0sub: {y0} ⊆ Y.
An exact proof term for the current goal is (singleton_subset y0 Y Hy0Y).
An exact proof term for the current goal is (setprod_Subq X {y0} X Y HXsub Hy0sub).
We prove the intermediate claim HunionAB: connected_space (⋃ {A,B}) (subspace_topology (setprod X Y) Top (⋃ {A,B})).
Apply (union_connected_common_point (setprod X Y) Top {A,B} HTprod) to the current goal.
An exact proof term for the current goal is HABsub.
Let D be given.
Assume HD: D ∈ {A,B}.
Apply (UPairE D A B HD (connected_space D (subspace_topology (setprod X Y) Top D))) to the current goal.
Assume HDa: D = A.
rewrite the current goal using HDa (from left to right).
An exact proof term for the current goal is HAconn.
Assume HDb: D = B.
rewrite the current goal using HDb (from left to right).
An exact proof term for the current goal is HBconn.
We use (x,y0) to witness the existential quantifier.
Let D be given.
Assume HD: D ∈ {A,B}.
Apply (UPairE D A B HD ((x,y0) ∈ D)) to the current goal.
Assume HDa: D = A.
rewrite the current goal using HDa (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {x} Y x y0 (SingI x) Hy0Y).
Assume HDb: D = B.
rewrite the current goal using HDb (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X {y0} x y0 HxX (SingI y0)).
rewrite the current goal using (binunion_eq_Union_pair A B) (from left to right).
An exact proof term for the current goal is HunionAB.
We prove the intermediate claim Hcommon: ∃p : set, ∀C : set, C ∈ F → p ∈ C.
We use (x0,y0) to witness the existential quantifier.
Let C be given.
Assume HC: C ∈ F.
Apply (ReplE_impred X (λx : set ⇒ setprod {x} Y ∪ Hhor) C HC) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume HCeq: C = setprod {x} Y ∪ Hhor.
rewrite the current goal using HCeq (from left to right).
We will prove (x0,y0) ∈ setprod {x} Y ∪ Hhor.
Apply binunionI2 to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X {y0} x0 y0 Hx0X (SingI y0)).
We prove the intermediate claim HconnUnion: connected_space (⋃ F) (subspace_topology (setprod X Y) Top (⋃ F)).
An exact proof term for the current goal is (union_connected_common_point (setprod X Y) Top F HTprod HFsub HFconn Hcommon).
We prove the intermediate claim HFpow: F ⊆ 𝒫 (setprod X Y).
Let C be given.
Assume HC: C ∈ F.
We will prove C ∈ 𝒫 (setprod X Y).
An exact proof term for the current goal is (PowerI (setprod X Y) C (HFsub C HC)).
We prove the intermediate claim HUnionSub: ⋃ F ⊆ setprod X Y.
An exact proof term for the current goal is (Union_Power (setprod X Y) F HFpow).
We prove the intermediate claim HSubUnion: setprod X Y ⊆ ⋃ F.
Let p be given.
Assume Hp: p ∈ setprod X Y.
We prove the intermediate claim Hp0X: (p 0) ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ Y) p Hp).
We prove the intermediate claim Hp1Y: (p 1) ∈ Y.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ Y) p Hp).
Set C0 to be the term setprod {p 0} Y ∪ Hhor.
We prove the intermediate claim HC0F: C0 ∈ F.
An exact proof term for the current goal is (ReplI X (λx : set ⇒ setprod {x} Y ∪ Hhor) (p 0) Hp0X).
We will prove p ∈ ⋃ F.
Apply (UnionI F p C0) to the current goal.
We will prove p ∈ C0.
Apply binunionI1 to the current goal.
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta X Y p Hp).
rewrite the current goal using Heta (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {p 0} Y (p 0) (p 1) (SingI (p 0)) Hp1Y).
An exact proof term for the current goal is HC0F.
We prove the intermediate claim HUnionEq: ⋃ F = setprod X Y.
Apply set_ext to the current goal.
An exact proof term for the current goal is HUnionSub.
An exact proof term for the current goal is HSubUnion.
We prove the intermediate claim HconnAmbientSub: connected_space (setprod X Y) (subspace_topology (setprod X Y) Top (setprod X Y)).
rewrite the current goal using HUnionEq (from right to left).
An exact proof term for the current goal is HconnUnion.
We prove the intermediate claim Hsubeq: subspace_topology (setprod X Y) Top (setprod X Y) = Top.
An exact proof term for the current goal is (subspace_topology_whole (setprod X Y) Top HTprod).
rewrite the current goal using Hsubeq (from right to left).
An exact proof term for the current goal is HconnAmbientSub.
∎