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

Theorem txconn 21540
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 21268 . . 3 (𝑅 ∈ Conn → 𝑅 ∈ Top)
2 conntop 21268 . . 3 (𝑆 ∈ Conn → 𝑆 ∈ Top)
3 txtop 21420 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
41, 2, 3syl2an 493 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Top)
5 neq0 3963 . . . . . . 7 𝑥 = ∅ ↔ ∃𝑧 𝑧𝑥)
6 inss1 3866 . . . . . . . . . . . 12 ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ (𝑅 ×t 𝑆)
7 simplr 807 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
86, 7sseldi 3634 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆))
9 elssuni 4499 . . . . . . . . . . 11 (𝑥 ∈ (𝑅 ×t 𝑆) → 𝑥 (𝑅 ×t 𝑆))
108, 9syl 17 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 (𝑅 ×t 𝑆))
11 simprr 811 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 (𝑅 ×t 𝑆))
12 simplll 813 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Conn)
1312, 1syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ Top)
14 simpllr 815 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Conn)
1514, 2syl 17 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ Top)
16 eqid 2651 . . . . . . . . . . . . . . . . 17 𝑅 = 𝑅
17 eqid 2651 . . . . . . . . . . . . . . . . 17 𝑆 = 𝑆
1816, 17txuni 21443 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
1913, 15, 18syl2anc 694 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ( 𝑅 × 𝑆) = (𝑅 ×t 𝑆))
2011, 19eleqtrrd 2733 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 ∈ ( 𝑅 × 𝑆))
21 1st2nd2 7249 . . . . . . . . . . . . . 14 (𝑤 ∈ ( 𝑅 × 𝑆) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
2220, 21syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
23 xp2nd 7243 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ( 𝑅 × 𝑆) → (2nd𝑤) ∈ 𝑆)
2420, 23syl 17 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ 𝑆)
25 eqid 2651 . . . . . . . . . . . . . . . . . 18 (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) = (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩)
2625mptpreima 5666 . . . . . . . . . . . . . . . . 17 ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) = {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥}
2717toptopon 20770 . . . . . . . . . . . . . . . . . . . 20 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘ 𝑆))
2815, 27sylib 208 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘ 𝑆))
2916toptopon 20770 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
3013, 29sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘ 𝑅))
31 xp1st 7242 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ( 𝑅 × 𝑆) → (1st𝑤) ∈ 𝑅)
3220, 31syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ 𝑅)
3328, 30, 32cnmptc 21513 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ (1st𝑤)) ∈ (𝑆 Cn 𝑅))
3428cnmptid 21512 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆𝑎) ∈ (𝑆 Cn 𝑆))
3528, 33, 34cnmpt1t 21516 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)))
36 simplr 807 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))))
376, 36sseldi 3634 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆))
38 cnima 21117 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
3935, 37, 38syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ 𝑆)
4026, 39syl5eqelr 2735 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ 𝑆)
41 simprl 809 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧𝑥)
42 elunii 4473 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧𝑥𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 (𝑅 ×t 𝑆))
4341, 37, 42syl2anc 694 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 (𝑅 ×t 𝑆))
4443, 19eleqtrrd 2733 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 ∈ ( 𝑅 × 𝑆))
45 xp2nd 7243 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ( 𝑅 × 𝑆) → (2nd𝑧) ∈ 𝑆)
4644, 45syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑧) ∈ 𝑆)
47 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) = (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩)
4847mptpreima 5666 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) = {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥}
4930cnmptid 21512 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅𝑎) ∈ (𝑅 Cn 𝑅))
5030, 28, 46cnmptc 21513 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ (2nd𝑧)) ∈ (𝑅 Cn 𝑆))
5130, 49, 50cnmpt1t 21516 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)))
52 cnima 21117 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5351, 37, 52syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ 𝑅)
5448, 53syl5eqelr 2735 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ 𝑅)
55 xp1st 7242 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ ( 𝑅 × 𝑆) → (1st𝑧) ∈ 𝑅)
5644, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑧) ∈ 𝑅)
57 1st2nd2 7249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ ( 𝑅 × 𝑆) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5844, 57syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
5958, 41eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥)
60 opeq1 4433 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = (1st𝑧) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑧), (2nd𝑧)⟩)
6160eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (1st𝑧) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥))
6261rspcev 3340 . . . . . . . . . . . . . . . . . . . . . . 23 (((1st𝑧) ∈ 𝑅 ∧ ⟨(1st𝑧), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6356, 59, 62syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
64 rabn0 3991 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑅𝑎, (2nd𝑧)⟩ ∈ 𝑥)
6563, 64sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ≠ ∅)
66 inss2 3867 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ (Clsd‘(𝑅 ×t 𝑆))
6766, 36sseldi 3634 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆)))
68 cnclima 21120 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
6951, 67, 68syl2anc 694 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑅 ↦ ⟨𝑎, (2nd𝑧)⟩) “ 𝑥) ∈ (Clsd‘𝑅))
7048, 69syl5eqelr 2735 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ∈ (Clsd‘𝑅))
7116, 12, 54, 65, 70connclo 21266 . . . . . . . . . . . . . . . . . . . 20 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} = 𝑅)
7232, 71eleqtrrd 2733 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥})
73 opeq1 4433 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎 = (1st𝑤) → ⟨𝑎, (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7473eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = (1st𝑤) → (⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7574elrab 3396 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} ↔ ((1st𝑤) ∈ 𝑅 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
7675simprbi 479 . . . . . . . . . . . . . . . . . . 19 ((1st𝑤) ∈ {𝑎 𝑅 ∣ ⟨𝑎, (2nd𝑧)⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
7772, 76syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥)
78 opeq2 4434 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = (2nd𝑧) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑧)⟩)
7978eleq1d 2715 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (2nd𝑧) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥))
8079rspcev 3340 . . . . . . . . . . . . . . . . . 18 (((2nd𝑧) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑧)⟩ ∈ 𝑥) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8146, 77, 80syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
82 rabn0 3991 . . . . . . . . . . . . . . . . 17 ({𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 𝑆⟨(1st𝑤), 𝑎⟩ ∈ 𝑥)
8381, 82sylibr 224 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ≠ ∅)
84 cnclima 21120 . . . . . . . . . . . . . . . . . 18 (((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8535, 67, 84syl2anc 694 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ((𝑎 𝑆 ↦ ⟨(1st𝑤), 𝑎⟩) “ 𝑥) ∈ (Clsd‘𝑆))
8626, 85syl5eqelr 2735 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ∈ (Clsd‘𝑆))
8717, 14, 40, 83, 86connclo 21266 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} = 𝑆)
8824, 87eleqtrrd 2733 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → (2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥})
89 opeq2 4434 . . . . . . . . . . . . . . . . 17 (𝑎 = (2nd𝑤) → ⟨(1st𝑤), 𝑎⟩ = ⟨(1st𝑤), (2nd𝑤)⟩)
9089eleq1d 2715 . . . . . . . . . . . . . . . 16 (𝑎 = (2nd𝑤) → (⟨(1st𝑤), 𝑎⟩ ∈ 𝑥 ↔ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
9190elrab 3396 . . . . . . . . . . . . . . 15 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} ↔ ((2nd𝑤) ∈ 𝑆 ∧ ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥))
9291simprbi 479 . . . . . . . . . . . . . 14 ((2nd𝑤) ∈ {𝑎 𝑆 ∣ ⟨(1st𝑤), 𝑎⟩ ∈ 𝑥} → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9388, 92syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → ⟨(1st𝑤), (2nd𝑤)⟩ ∈ 𝑥)
9422, 93eqeltrd 2730 . . . . . . . . . . . 12 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧𝑥𝑤 (𝑅 ×t 𝑆))) → 𝑤𝑥)
9594expr 642 . . . . . . . . . . 11 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑤 (𝑅 ×t 𝑆) → 𝑤𝑥))
9695ssrdv 3642 . . . . . . . . . 10 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → (𝑅 ×t 𝑆) ⊆ 𝑥)
9710, 96eqssd 3653 . . . . . . . . 9 ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧𝑥) → 𝑥 = (𝑅 ×t 𝑆))
9897ex 449 . . . . . . . 8 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
9998exlimdv 1901 . . . . . . 7 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (∃𝑧 𝑧𝑥𝑥 = (𝑅 ×t 𝑆)))
1005, 99syl5bi 232 . . . . . 6 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (¬ 𝑥 = ∅ → 𝑥 = (𝑅 ×t 𝑆)))
101100orrd 392 . . . . 5 (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
102101ex 449 . . . 4 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆))))
103 vex 3234 . . . . 5 𝑥 ∈ V
104103elpr 4231 . . . 4 (𝑥 ∈ {∅, (𝑅 ×t 𝑆)} ↔ (𝑥 = ∅ ∨ 𝑥 = (𝑅 ×t 𝑆)))
105102, 104syl6ibr 242 . . 3 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, (𝑅 ×t 𝑆)}))
106105ssrdv 3642 . 2 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)})
107 eqid 2651 . . 3 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
108107isconn2 21265 . 2 ((𝑅 ×t 𝑆) ∈ Conn ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, (𝑅 ×t 𝑆)}))
1094, 106, 108sylanbrc 699 1 ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1523  wex 1744  wcel 2030  wne 2823  wrex 2942  {crab 2945  cin 3606  wss 3607  c0 3948  {cpr 4212  cop 4216   cuni 4468  cmpt 4762   × cxp 5141  ccnv 5142  cima 5146  cfv 5926  (class class class)co 6690  1st c1st 7208  2nd c2nd 7209  Topctop 20746  TopOnctopon 20763  Clsdccld 20868   Cn ccn 21076  Conncconn 21262   ×t ctx 21411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-map 7901  df-topgen 16151  df-top 20747  df-topon 20764  df-bases 20798  df-cld 20871  df-cn 21079  df-cnp 21080  df-conn 21263  df-tx 21413
This theorem is referenced by:  cvmlift2lem9  31419  cvmlift2lem13  31423
  Copyright terms: Public domain W3C validator