MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txconn Structured version   Visualization version   GIF version

Theorem txconn 23718
Description: The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.)
Assertion
Ref Expression
txconn ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)

Proof of Theorem txconn
Dummy variables 𝑤 𝑎 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 conntop 23446 . . 3 (𝑅 ∈ Conn → 𝑅 ∈ Top)
2 conntop 23446 . . 3 (𝑆 ∈ Conn → 𝑆 ∈ Top)
3 txtop 23598 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 595 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Top)
5 neq0 4375 . . . . . . 7 𝑥 = ∅ ↔ ∃𝑧 𝑧𝑥)
6 simplr 768 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
76elin1d 4227 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆))
8 elssuni 4961 . . . . . . . . . . 11 (𝑥 ∈ (𝑅 ×t 𝑆) → 𝑥 (𝑅 ×t 𝑆))
97, 8syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 (𝑅 ×t 𝑆))
10 simprr 772 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 (𝑅 ×t 𝑆))
11 simplll 774 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Conn)
1211, 1syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Top)
13 simpllr 775 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Conn)
1413, 2syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Top)
15 eqid 2740 . . . . . . . . . . . . . . . . 17 𝑅 = 𝑅
16 eqid 2740 . . . . . . . . . . . . . . . . 17 𝑆 = 𝑆
1715, 16txuni 23621 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1812, 14, 17syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1910, 18eleqtrrd 2847 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 ∈ ( 𝑅 × 𝑆))
20 1st2nd2 8069 . . . . . . . . . . . . . 14 (𝑤 ∈ ( 𝑅 × 𝑆) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
2119, 20syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
22 xp2nd 8063 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ( 𝑅 × 𝑆) → (2nd𝑤) ∈ 𝑆)
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ 𝑆)
24 eqid 2740 . . . . . . . . . . . . . . . . . 18 (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) = (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩)
2524mptpreima 6269 . . . . . . . . . . . . . . . . 17 ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) = {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥}
26 toptopon2 22945 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2714, 26sylib 218 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘ 𝑆))
28 toptopon2 22945 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
2912, 28sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘ 𝑅))
30 xp1st 8062 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ( 𝑅 × 𝑆) → (1st𝑤) ∈ 𝑅)
3119, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ 𝑅)
3227, 29, 31cnmptc 23691 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ (1st𝑤)) ∈ (𝑆 Cn 𝑅))
3327cnmptid 23690 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆𝑎) ∈ (𝑆 Cn 𝑆))
3427, 32, 33cnmpt1t 23694 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)))
35 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
3635elin1d 4227 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
37 cnima 23294 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3834, 36, 37syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3925, 38eqeltrrid 2849 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ 𝑆)
40 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧𝑥)
41 elunii 4936 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑥𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 (𝑅 ×t 𝑆))
4240, 36, 41syl2anc 583 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 (𝑅 ×t 𝑆))
4342, 18eleqtrrd 2847 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 ∈ ( 𝑅 × 𝑆))
44 xp2nd 8063 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ( 𝑅 × 𝑆) → (2nd𝑧) ∈ 𝑆)
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑧) ∈ 𝑆)
46 eqid 2740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) = (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩)
4746mptpreima 6269 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) = {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥}
4829cnmptid 23690 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅𝑎) ∈ (𝑅 Cn 𝑅))
4929, 27, 45cnmptc 23691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ (2nd𝑧)) ∈ (𝑅 Cn 𝑆))
5029, 48, 49cnmpt1t 23694 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
51 cnima 23294 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5250, 36, 51syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5347, 52eqeltrrid 2849 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ 𝑅)
54 xp1st 8062 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ( 𝑅 × 𝑆) → (1st𝑧) ∈ 𝑅)
5543, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑧) ∈ 𝑅)
56 1st2nd2 8069 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ( 𝑅 × 𝑆) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5743, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5857, 40eqeltrrd 2845 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥)
59 opeq1 4897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (1st𝑧) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
6059eleq1d 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (1st𝑧) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥))
6160rspcev 3635 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∈ 𝑅 ∧ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6255, 58, 61syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
63 rabn0 4412 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6462, 63sylibr 234 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅)
6535elin2d 4228 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆)))
66 cnclima 23297 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6750, 65, 66syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6847, 67eqeltrrid 2849 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ (Clsd‘𝑅))
6915, 11, 53, 64, 68connclo 23444 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} = 𝑅)
7031, 69eleqtrrd 2847 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥})
71 opeq1 4897 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (1st𝑤) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7271eleq1d 2829 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (1st𝑤) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7372elrab 3708 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ↔ ((1st𝑤) ∈ 𝑅 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7473simprbi 496 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
7570, 74syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
76 opeq2 4898 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (2nd𝑧) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7776eleq1d 2829 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (2nd𝑧) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7877rspcev 3635 . . . . . . . . . . . . . . . . . 18 (((2nd𝑧) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
7945, 75, 78syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
80 rabn0 4412 . . . . . . . . . . . . . . . . 17 ({𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8179, 80sylibr 234 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅)
82 cnclima 23297 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8334, 65, 82syl2anc 583 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8425, 83eqeltrrid 2849 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ (Clsd‘𝑆))
8516, 13, 39, 81, 84connclo 23444 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} = 𝑆)
8623, 85eleqtrrd 2847 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥})
87 opeq2 4898 . . . . . . . . . . . . . . . . 17 (𝑎 = (2nd𝑤) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑤)⟩)
8887eleq1d 2829 . . . . . . . . . . . . . . . 16 (𝑎 = (2nd𝑤) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
8988elrab 3708 . . . . . . . . . . . . . . 15 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ↔ ((2nd𝑤) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
9089simprbi 496 . . . . . . . . . . . . . 14 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9186, 90syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9221, 91eqeltrd 2844 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤𝑥)
9392expr 456 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑤 (𝑅 ×t 𝑆) → 𝑤𝑥))
9493ssrdv 4014 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑅 ×t 𝑆) ⊆ 𝑥)
959, 94eqssd 4026 . . . . . . . . 9 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 = (𝑅 ×t 𝑆))
9695ex 412 . . . . . . . 8 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
9796exlimdv 1932 . . . . . . 7 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (∃𝑧 𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
985, 97biimtrid 242 . . . . . 6 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (¬ 𝑥 = ∅ → 𝑥 = (𝑅 ×t 𝑆)))
9998orrd 862 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
10099ex 412 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆))))
101 vex 3492 . . . . 5 𝑥 ∈ V
102101elpr 4672 . . . 4 (𝑥 ∈ {∅, (𝑅 ×t 𝑆)} ↔ (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
103100, 102imbitrrdi 252 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, (𝑅 ×t 𝑆)}))
104103ssrdv 4014 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)})
105 eqid 2740 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
106105isconn2 23443 . 2 ((𝑅 ×t 𝑆) ∈ Conn ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)}))
1074, 104, 106sylanbrc 582 1 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 846   = wceq 1537  wex 1777  wcel 2108  wne 2946  wrex 3076  {crab 3443  cin 3975  wss 3976  c0 4352  {cpr 4650  cop 4654   cuni 4931  cmpt 5249   × cxp 5698  ccnv 5699  cima 5703  cfv 6573  (class class class)co 7448  1st c1st 8028  2nd c2nd 8029  Topctop 22920  TopOnctopon 22937  Clsdccld 23045   Cn ccn 23253  Conncconn 23440   ×t ctx 23589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-map 8886  df-topgen 17503  df-top 22921  df-topon 22938  df-bases 22974  df-cld 23048  df-cn 23256  df-cnp 23257  df-conn 23441  df-tx 23591
This theorem is referenced by:  cvmlift2lem9  35279  cvmlift2lem13  35283
  Copyright terms: Public domain W3C validator