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

Theorem txconn 21486
 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 21214 . . 3 (𝑅 ∈ Conn → 𝑅 ∈ Top)
2 conntop 21214 . . 3 (𝑆 ∈ Conn → 𝑆 ∈ Top)
3 txtop 21366 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 494 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Top)
5 neq0 3928 . . . . . . 7 𝑥 = ∅ ↔ ∃𝑧 𝑧𝑥)
6 inss1 3831 . . . . . . . . . . . 12 ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ (𝑅 ×t 𝑆)
7 simplr 792 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
86, 7sseldi 3599 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆))
9 elssuni 4465 . . . . . . . . . . 11 (𝑥 ∈ (𝑅 ×t 𝑆) → 𝑥 (𝑅 ×t 𝑆))
108, 9syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 (𝑅 ×t 𝑆))
11 simprr 796 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 (𝑅 ×t 𝑆))
12 simplll 798 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Conn)
1312, 1syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Top)
14 simpllr 799 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Conn)
1514, 2syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Top)
16 eqid 2621 . . . . . . . . . . . . . . . . 17 𝑅 = 𝑅
17 eqid 2621 . . . . . . . . . . . . . . . . 17 𝑆 = 𝑆
1816, 17txuni 21389 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1913, 15, 18syl2anc 693 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2011, 19eleqtrrd 2703 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 ∈ ( 𝑅 × 𝑆))
21 1st2nd2 7202 . . . . . . . . . . . . . 14 (𝑤 ∈ ( 𝑅 × 𝑆) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
2220, 21syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
23 xp2nd 7196 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ( 𝑅 × 𝑆) → (2nd𝑤) ∈ 𝑆)
2420, 23syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ 𝑆)
25 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) = (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩)
2625mptpreima 5626 . . . . . . . . . . . . . . . . 17 ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) = {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥}
2717toptopon 20716 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2815, 27sylib 208 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘ 𝑆))
2916toptopon 20716 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
3013, 29sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘ 𝑅))
31 xp1st 7195 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ( 𝑅 × 𝑆) → (1st𝑤) ∈ 𝑅)
3220, 31syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ 𝑅)
3328, 30, 32cnmptc 21459 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ (1st𝑤)) ∈ (𝑆 Cn 𝑅))
3428cnmptid 21458 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆𝑎) ∈ (𝑆 Cn 𝑆))
3528, 33, 34cnmpt1t 21462 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)))
36 simplr 792 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
376, 36sseldi 3599 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
38 cnima 21063 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3935, 37, 38syl2anc 693 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
4026, 39syl5eqelr 2705 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ 𝑆)
41 simprl 794 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧𝑥)
42 elunii 4439 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑥𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 (𝑅 ×t 𝑆))
4341, 37, 42syl2anc 693 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 (𝑅 ×t 𝑆))
4443, 19eleqtrrd 2703 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 ∈ ( 𝑅 × 𝑆))
45 xp2nd 7196 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ( 𝑅 × 𝑆) → (2nd𝑧) ∈ 𝑆)
4644, 45syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑧) ∈ 𝑆)
47 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) = (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩)
4847mptpreima 5626 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) = {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥}
4930cnmptid 21458 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅𝑎) ∈ (𝑅 Cn 𝑅))
5030, 28, 46cnmptc 21459 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ (2nd𝑧)) ∈ (𝑅 Cn 𝑆))
5130, 49, 50cnmpt1t 21462 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
52 cnima 21063 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5351, 37, 52syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5448, 53syl5eqelr 2705 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ 𝑅)
55 xp1st 7195 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ( 𝑅 × 𝑆) → (1st𝑧) ∈ 𝑅)
5644, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑧) ∈ 𝑅)
57 1st2nd2 7202 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ( 𝑅 × 𝑆) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5844, 57syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5958, 41eqeltrrd 2701 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥)
60 opeq1 4400 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (1st𝑧) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
6160eleq1d 2685 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (1st𝑧) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥))
6261rspcev 3307 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∈ 𝑅 ∧ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6356, 59, 62syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
64 rabn0 3956 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6563, 64sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅)
66 inss2 3832 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ (Clsd‘(𝑅 ×t 𝑆))
6766, 36sseldi 3599 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆)))
68 cnclima 21066 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6951, 67, 68syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
7048, 69syl5eqelr 2705 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ (Clsd‘𝑅))
7116, 12, 54, 65, 70connclo 21212 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} = 𝑅)
7232, 71eleqtrrd 2703 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥})
73 opeq1 4400 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (1st𝑤) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7473eleq1d 2685 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (1st𝑤) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7574elrab 3361 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ↔ ((1st𝑤) ∈ 𝑅 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7675simprbi 480 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
7772, 76syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
78 opeq2 4401 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (2nd𝑧) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7978eleq1d 2685 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (2nd𝑧) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
8079rspcev 3307 . . . . . . . . . . . . . . . . . 18 (((2nd𝑧) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8146, 77, 80syl2anc 693 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
82 rabn0 3956 . . . . . . . . . . . . . . . . 17 ({𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8381, 82sylibr 224 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅)
84 cnclima 21066 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8535, 67, 84syl2anc 693 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8626, 85syl5eqelr 2705 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ (Clsd‘𝑆))
8717, 14, 40, 83, 86connclo 21212 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} = 𝑆)
8824, 87eleqtrrd 2703 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥})
89 opeq2 4401 . . . . . . . . . . . . . . . . 17 (𝑎 = (2nd𝑤) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑤)⟩)
9089eleq1d 2685 . . . . . . . . . . . . . . . 16 (𝑎 = (2nd𝑤) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
9190elrab 3361 . . . . . . . . . . . . . . 15 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ↔ ((2nd𝑤) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
9291simprbi 480 . . . . . . . . . . . . . 14 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9388, 92syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9422, 93eqeltrd 2700 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤𝑥)
9594expr 643 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑤 (𝑅 ×t 𝑆) → 𝑤𝑥))
9695ssrdv 3607 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑅 ×t 𝑆) ⊆ 𝑥)
9710, 96eqssd 3618 . . . . . . . . 9 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 = (𝑅 ×t 𝑆))
9897ex 450 . . . . . . . 8 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
9998exlimdv 1860 . . . . . . 7 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (∃𝑧 𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
1005, 99syl5bi 232 . . . . . 6 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (¬ 𝑥 = ∅ → 𝑥 = (𝑅 ×t 𝑆)))
101100orrd 393 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
102101ex 450 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆))))
103 vex 3201 . . . . 5 𝑥 ∈ V
104103elpr 4196 . . . 4 (𝑥 ∈ {∅, (𝑅 ×t 𝑆)} ↔ (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
105102, 104syl6ibr 242 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, (𝑅 ×t 𝑆)}))
106105ssrdv 3607 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)})
107 eqid 2621 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
108107isconn2 21211 . 2 ((𝑅 ×t 𝑆) ∈ Conn ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)}))
1094, 106, 108sylanbrc 698 1 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1482  ∃wex 1703   ∈ wcel 1989   ≠ wne 2793  ∃wrex 2912  {crab 2915   ∩ cin 3571   ⊆ wss 3572  ∅c0 3913  {cpr 4177  ⟨cop 4181  ∪ cuni 4434   ↦ cmpt 4727   × cxp 5110  ◡ccnv 5111   “ cima 5115  ‘cfv 5886  (class class class)co 6647  1st c1st 7163  2nd c2nd 7164  Topctop 20692  TopOnctopon 20709  Clsdccld 20814   Cn ccn 21022  Conncconn 21208   ×t ctx 21357 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-id 5022  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-ov 6650  df-oprab 6651  df-mpt2 6652  df-1st 7165  df-2nd 7166  df-map 7856  df-topgen 16098  df-top 20693  df-topon 20710  df-bases 20744  df-cld 20817  df-cn 21025  df-cnp 21026  df-conn 21209  df-tx 21359 This theorem is referenced by:  cvmlift2lem9  31278  cvmlift2lem13  31282
 Copyright terms: Public domain W3C validator