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

Theorem txconn 23698
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 23426 . . 3 (𝑅 ∈ Conn → 𝑅 ∈ Top)
2 conntop 23426 . . 3 (𝑆 ∈ Conn → 𝑆 ∈ Top)
3 txtop 23578 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 596 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Top)
5 neq0 4351 . . . . . . 7 𝑥 = ∅ ↔ ∃𝑧 𝑧𝑥)
6 simplr 768 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
76elin1d 4203 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆))
8 elssuni 4936 . . . . . . . . . . 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 2736 . . . . . . . . . . . . . . . . 17 𝑅 = 𝑅
16 eqid 2736 . . . . . . . . . . . . . . . . 17 𝑆 = 𝑆
1715, 16txuni 23601 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1812, 14, 17syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1910, 18eleqtrrd 2843 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 ∈ ( 𝑅 × 𝑆))
20 1st2nd2 8054 . . . . . . . . . . . . . 14 (𝑤 ∈ ( 𝑅 × 𝑆) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
2119, 20syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
22 xp2nd 8048 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ( 𝑅 × 𝑆) → (2nd𝑤) ∈ 𝑆)
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ 𝑆)
24 eqid 2736 . . . . . . . . . . . . . . . . . 18 (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) = (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩)
2524mptpreima 6257 . . . . . . . . . . . . . . . . 17 ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) = {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥}
26 toptopon2 22925 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2714, 26sylib 218 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘ 𝑆))
28 toptopon2 22925 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
2912, 28sylib 218 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘ 𝑅))
30 xp1st 8047 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ( 𝑅 × 𝑆) → (1st𝑤) ∈ 𝑅)
3119, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ 𝑅)
3227, 29, 31cnmptc 23671 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ (1st𝑤)) ∈ (𝑆 Cn 𝑅))
3327cnmptid 23670 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆𝑎) ∈ (𝑆 Cn 𝑆))
3427, 32, 33cnmpt1t 23674 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)))
35 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
3635elin1d 4203 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
37 cnima 23274 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3834, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3925, 38eqeltrrid 2845 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ 𝑆)
40 simprl 770 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧𝑥)
41 elunii 4911 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑥𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 (𝑅 ×t 𝑆))
4240, 36, 41syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 (𝑅 ×t 𝑆))
4342, 18eleqtrrd 2843 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 ∈ ( 𝑅 × 𝑆))
44 xp2nd 8048 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ( 𝑅 × 𝑆) → (2nd𝑧) ∈ 𝑆)
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑧) ∈ 𝑆)
46 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) = (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩)
4746mptpreima 6257 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) = {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥}
4829cnmptid 23670 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅𝑎) ∈ (𝑅 Cn 𝑅))
4929, 27, 45cnmptc 23671 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ (2nd𝑧)) ∈ (𝑅 Cn 𝑆))
5029, 48, 49cnmpt1t 23674 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
51 cnima 23274 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5250, 36, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5347, 52eqeltrrid 2845 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ 𝑅)
54 xp1st 8047 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ( 𝑅 × 𝑆) → (1st𝑧) ∈ 𝑅)
5543, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑧) ∈ 𝑅)
56 1st2nd2 8054 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ( 𝑅 × 𝑆) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5743, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5857, 40eqeltrrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥)
59 opeq1 4872 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (1st𝑧) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
6059eleq1d 2825 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (1st𝑧) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥))
6160rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∈ 𝑅 ∧ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6255, 58, 61syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
63 rabn0 4388 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6462, 63sylibr 234 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅)
6535elin2d 4204 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆)))
66 cnclima 23277 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6750, 65, 66syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6847, 67eqeltrrid 2845 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ (Clsd‘𝑅))
6915, 11, 53, 64, 68connclo 23424 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} = 𝑅)
7031, 69eleqtrrd 2843 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥})
71 opeq1 4872 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (1st𝑤) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7271eleq1d 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (1st𝑤) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7372elrab 3691 . . . . . . . . . . . . . . . . . . . 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 4873 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (2nd𝑧) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7776eleq1d 2825 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (2nd𝑧) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7877rspcev 3621 . . . . . . . . . . . . . . . . . 18 (((2nd𝑧) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
7945, 75, 78syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
80 rabn0 4388 . . . . . . . . . . . . . . . . 17 ({𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8179, 80sylibr 234 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅)
82 cnclima 23277 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8334, 65, 82syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8425, 83eqeltrrid 2845 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ (Clsd‘𝑆))
8516, 13, 39, 81, 84connclo 23424 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} = 𝑆)
8623, 85eleqtrrd 2843 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥})
87 opeq2 4873 . . . . . . . . . . . . . . . . 17 (𝑎 = (2nd𝑤) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑤)⟩)
8887eleq1d 2825 . . . . . . . . . . . . . . . 16 (𝑎 = (2nd𝑤) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
8988elrab 3691 . . . . . . . . . . . . . . 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 2840 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤𝑥)
9392expr 456 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑤 (𝑅 ×t 𝑆) → 𝑤𝑥))
9493ssrdv 3988 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑅 ×t 𝑆) ⊆ 𝑥)
959, 94eqssd 4000 . . . . . . . . 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 863 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
10099ex 412 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆))))
101 vex 3483 . . . . 5 𝑥 ∈ V
102101elpr 4649 . . . 4 (𝑥 ∈ {∅, (𝑅 ×t 𝑆)} ↔ (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
103100, 102imbitrrdi 252 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, (𝑅 ×t 𝑆)}))
104103ssrdv 3988 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)})
105 eqid 2736 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
106105isconn2 23423 . 2 ((𝑅 ×t 𝑆) ∈ Conn ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)}))
1074, 104, 106sylanbrc 583 1 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847   = wceq 1539  wex 1778  wcel 2107  wne 2939  wrex 3069  {crab 3435  cin 3949  wss 3950  c0 4332  {cpr 4627  cop 4631   cuni 4906  cmpt 5224   × cxp 5682  ccnv 5683  cima 5687  cfv 6560  (class class class)co 7432  1st c1st 8013  2nd c2nd 8014  Topctop 22900  TopOnctopon 22917  Clsdccld 23025   Cn ccn 23233  Conncconn 23420   ×t ctx 23569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-ov 7435  df-oprab 7436  df-mpo 7437  df-1st 8015  df-2nd 8016  df-map 8869  df-topgen 17489  df-top 22901  df-topon 22918  df-bases 22954  df-cld 23028  df-cn 23236  df-cnp 23237  df-conn 23421  df-tx 23571
This theorem is referenced by:  cvmlift2lem9  35317  cvmlift2lem13  35321
  Copyright terms: Public domain W3C validator