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

Theorem txconn 22225
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 21953 . . 3 (𝑅 ∈ Conn → 𝑅 ∈ Top)
2 conntop 21953 . . 3 (𝑆 ∈ Conn → 𝑆 ∈ Top)
3 txtop 22105 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 595 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Top)
5 neq0 4306 . . . . . . 7 𝑥 = ∅ ↔ ∃𝑧 𝑧𝑥)
6 simplr 765 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
76elin1d 4172 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆))
8 elssuni 4859 . . . . . . . . . . 11 (𝑥 ∈ (𝑅 ×t 𝑆) → 𝑥 (𝑅 ×t 𝑆))
97, 8syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 (𝑅 ×t 𝑆))
10 simprr 769 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 (𝑅 ×t 𝑆))
11 simplll 771 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Conn)
1211, 1syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Top)
13 simpllr 772 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Conn)
1413, 2syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Top)
15 eqid 2818 . . . . . . . . . . . . . . . . 17 𝑅 = 𝑅
16 eqid 2818 . . . . . . . . . . . . . . . . 17 𝑆 = 𝑆
1715, 16txuni 22128 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1812, 14, 17syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1910, 18eleqtrrd 2913 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 ∈ ( 𝑅 × 𝑆))
20 1st2nd2 7717 . . . . . . . . . . . . . 14 (𝑤 ∈ ( 𝑅 × 𝑆) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
2119, 20syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
22 xp2nd 7711 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ( 𝑅 × 𝑆) → (2nd𝑤) ∈ 𝑆)
2319, 22syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ 𝑆)
24 eqid 2818 . . . . . . . . . . . . . . . . . 18 (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) = (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩)
2524mptpreima 6085 . . . . . . . . . . . . . . . . 17 ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) = {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥}
26 toptopon2 21454 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2714, 26sylib 219 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘ 𝑆))
28 toptopon2 21454 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
2912, 28sylib 219 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘ 𝑅))
30 xp1st 7710 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ( 𝑅 × 𝑆) → (1st𝑤) ∈ 𝑅)
3119, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ 𝑅)
3227, 29, 31cnmptc 22198 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ (1st𝑤)) ∈ (𝑆 Cn 𝑅))
3327cnmptid 22197 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆𝑎) ∈ (𝑆 Cn 𝑆))
3427, 32, 33cnmpt1t 22201 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)))
35 simplr 765 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
3635elin1d 4172 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
37 cnima 21801 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3834, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3925, 38eqeltrrid 2915 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ 𝑆)
40 simprl 767 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧𝑥)
41 elunii 4835 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑥𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 (𝑅 ×t 𝑆))
4240, 36, 41syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 (𝑅 ×t 𝑆))
4342, 18eleqtrrd 2913 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 ∈ ( 𝑅 × 𝑆))
44 xp2nd 7711 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ( 𝑅 × 𝑆) → (2nd𝑧) ∈ 𝑆)
4543, 44syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑧) ∈ 𝑆)
46 eqid 2818 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) = (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩)
4746mptpreima 6085 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) = {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥}
4829cnmptid 22197 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅𝑎) ∈ (𝑅 Cn 𝑅))
4929, 27, 45cnmptc 22198 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ (2nd𝑧)) ∈ (𝑅 Cn 𝑆))
5029, 48, 49cnmpt1t 22201 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
51 cnima 21801 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5250, 36, 51syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5347, 52eqeltrrid 2915 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ 𝑅)
54 xp1st 7710 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ( 𝑅 × 𝑆) → (1st𝑧) ∈ 𝑅)
5543, 54syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑧) ∈ 𝑅)
56 1st2nd2 7717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ( 𝑅 × 𝑆) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5743, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5857, 40eqeltrrd 2911 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥)
59 opeq1 4795 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (1st𝑧) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
6059eleq1d 2894 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (1st𝑧) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥))
6160rspcev 3620 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∈ 𝑅 ∧ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6255, 58, 61syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
63 rabn0 4336 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6462, 63sylibr 235 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅)
6535elin2d 4173 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆)))
66 cnclima 21804 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6750, 65, 66syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6847, 67eqeltrrid 2915 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ (Clsd‘𝑅))
6915, 11, 53, 64, 68connclo 21951 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} = 𝑅)
7031, 69eleqtrrd 2913 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥})
71 opeq1 4795 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (1st𝑤) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7271eleq1d 2894 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (1st𝑤) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7372elrab 3677 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ↔ ((1st𝑤) ∈ 𝑅 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7473simprbi 497 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
7570, 74syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
76 opeq2 4796 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (2nd𝑧) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7776eleq1d 2894 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (2nd𝑧) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7877rspcev 3620 . . . . . . . . . . . . . . . . . 18 (((2nd𝑧) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
7945, 75, 78syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
80 rabn0 4336 . . . . . . . . . . . . . . . . 17 ({𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8179, 80sylibr 235 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅)
82 cnclima 21804 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8334, 65, 82syl2anc 584 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8425, 83eqeltrrid 2915 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ (Clsd‘𝑆))
8516, 13, 39, 81, 84connclo 21951 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} = 𝑆)
8623, 85eleqtrrd 2913 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥})
87 opeq2 4796 . . . . . . . . . . . . . . . . 17 (𝑎 = (2nd𝑤) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑤)⟩)
8887eleq1d 2894 . . . . . . . . . . . . . . . 16 (𝑎 = (2nd𝑤) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
8988elrab 3677 . . . . . . . . . . . . . . 15 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ↔ ((2nd𝑤) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
9089simprbi 497 . . . . . . . . . . . . . 14 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9186, 90syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9221, 91eqeltrd 2910 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤𝑥)
9392expr 457 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑤 (𝑅 ×t 𝑆) → 𝑤𝑥))
9493ssrdv 3970 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑅 ×t 𝑆) ⊆ 𝑥)
959, 94eqssd 3981 . . . . . . . . 9 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 = (𝑅 ×t 𝑆))
9695ex 413 . . . . . . . 8 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
9796exlimdv 1925 . . . . . . 7 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (∃𝑧 𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
985, 97syl5bi 243 . . . . . 6 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (¬ 𝑥 = ∅ → 𝑥 = (𝑅 ×t 𝑆)))
9998orrd 857 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
10099ex 413 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆))))
101 vex 3495 . . . . 5 𝑥 ∈ V
102101elpr 4580 . . . 4 (𝑥 ∈ {∅, (𝑅 ×t 𝑆)} ↔ (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
103100, 102syl6ibr 253 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, (𝑅 ×t 𝑆)}))
104103ssrdv 3970 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)})
105 eqid 2818 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
106105isconn2 21950 . 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 396  wo 841   = wceq 1528  wex 1771  wcel 2105  wne 3013  wrex 3136  {crab 3139  cin 3932  wss 3933  c0 4288  {cpr 4559  cop 4563   cuni 4830  cmpt 5137   × cxp 5546  ccnv 5547  cima 5551  cfv 6348  (class class class)co 7145  1st c1st 7676  2nd c2nd 7677  Topctop 21429  TopOnctopon 21446  Clsdccld 21552   Cn ccn 21760  Conncconn 21947   ×t ctx 22096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7678  df-2nd 7679  df-map 8397  df-topgen 16705  df-top 21430  df-topon 21447  df-bases 21482  df-cld 21555  df-cn 21763  df-cnp 21764  df-conn 21948  df-tx 22098
This theorem is referenced by:  cvmlift2lem9  32455  cvmlift2lem13  32459
  Copyright terms: Public domain W3C validator