Metamath Proof Explorer


Theorem txconn

Description: The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015)

Ref Expression
Assertion txconn ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) → ( 𝑅 ×t 𝑆 ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 conntop ( 𝑅 ∈ Conn → 𝑅 ∈ Top )
2 conntop ( 𝑆 ∈ Conn → 𝑆 ∈ Top )
3 txtop ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
4 1 2 3 syl2an ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
5 neq0 ( ¬ 𝑥 = ∅ ↔ ∃ 𝑧 𝑧𝑥 )
6 simplr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ 𝑧𝑥 ) → 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) )
7 6 elin1d ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ 𝑧𝑥 ) → 𝑥 ∈ ( 𝑅 ×t 𝑆 ) )
8 elssuni ( 𝑥 ∈ ( 𝑅 ×t 𝑆 ) → 𝑥 ( 𝑅 ×t 𝑆 ) )
9 7 8 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ 𝑧𝑥 ) → 𝑥 ( 𝑅 ×t 𝑆 ) )
10 simprr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑤 ( 𝑅 ×t 𝑆 ) )
11 simplll ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑅 ∈ Conn )
12 11 1 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑅 ∈ Top )
13 simpllr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑆 ∈ Conn )
14 13 2 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑆 ∈ Top )
15 eqid 𝑅 = 𝑅
16 eqid 𝑆 = 𝑆
17 15 16 txuni ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 × 𝑆 ) = ( 𝑅 ×t 𝑆 ) )
18 12 14 17 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑅 × 𝑆 ) = ( 𝑅 ×t 𝑆 ) )
19 10 18 eleqtrrd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑤 ∈ ( 𝑅 × 𝑆 ) )
20 1st2nd2 ( 𝑤 ∈ ( 𝑅 × 𝑆 ) → 𝑤 = ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
21 19 20 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑤 = ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
22 xp2nd ( 𝑤 ∈ ( 𝑅 × 𝑆 ) → ( 2nd𝑤 ) ∈ 𝑆 )
23 19 22 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 2nd𝑤 ) ∈ 𝑆 )
24 eqid ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) = ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ )
25 24 mptpreima ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) “ 𝑥 ) = { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 }
26 toptopon2 ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ 𝑆 ) )
27 14 26 sylib ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑆 ∈ ( TopOn ‘ 𝑆 ) )
28 toptopon2 ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑅 ) )
29 12 28 sylib ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑅 ∈ ( TopOn ‘ 𝑅 ) )
30 xp1st ( 𝑤 ∈ ( 𝑅 × 𝑆 ) → ( 1st𝑤 ) ∈ 𝑅 )
31 19 30 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 1st𝑤 ) ∈ 𝑅 )
32 27 29 31 cnmptc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 𝑆 ↦ ( 1st𝑤 ) ) ∈ ( 𝑆 Cn 𝑅 ) )
33 27 cnmptid ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 𝑆𝑎 ) ∈ ( 𝑆 Cn 𝑆 ) )
34 27 32 33 cnmpt1t ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) ∈ ( 𝑆 Cn ( 𝑅 ×t 𝑆 ) ) )
35 simplr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) )
36 35 elin1d ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑥 ∈ ( 𝑅 ×t 𝑆 ) )
37 cnima ( ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) ∈ ( 𝑆 Cn ( 𝑅 ×t 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ) → ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) “ 𝑥 ) ∈ 𝑆 )
38 34 36 37 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) “ 𝑥 ) ∈ 𝑆 )
39 25 38 eqeltrrid ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } ∈ 𝑆 )
40 simprl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑧𝑥 )
41 elunii ( ( 𝑧𝑥𝑥 ∈ ( 𝑅 ×t 𝑆 ) ) → 𝑧 ( 𝑅 ×t 𝑆 ) )
42 40 36 41 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑧 ( 𝑅 ×t 𝑆 ) )
43 42 18 eleqtrrd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑧 ∈ ( 𝑅 × 𝑆 ) )
44 xp2nd ( 𝑧 ∈ ( 𝑅 × 𝑆 ) → ( 2nd𝑧 ) ∈ 𝑆 )
45 43 44 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 2nd𝑧 ) ∈ 𝑆 )
46 eqid ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) = ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ )
47 46 mptpreima ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) “ 𝑥 ) = { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 }
48 29 cnmptid ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 𝑅𝑎 ) ∈ ( 𝑅 Cn 𝑅 ) )
49 29 27 45 cnmptc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 𝑅 ↦ ( 2nd𝑧 ) ) ∈ ( 𝑅 Cn 𝑆 ) )
50 29 48 49 cnmpt1t ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) )
51 cnima ( ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) ∧ 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ) → ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) “ 𝑥 ) ∈ 𝑅 )
52 50 36 51 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) “ 𝑥 ) ∈ 𝑅 )
53 47 52 eqeltrrid ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } ∈ 𝑅 )
54 xp1st ( 𝑧 ∈ ( 𝑅 × 𝑆 ) → ( 1st𝑧 ) ∈ 𝑅 )
55 43 54 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 1st𝑧 ) ∈ 𝑅 )
56 1st2nd2 ( 𝑧 ∈ ( 𝑅 × 𝑆 ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
57 43 56 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑧 = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
58 57 40 eqeltrrd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 )
59 opeq1 ( 𝑎 = ( 1st𝑧 ) → ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ = ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ )
60 59 eleq1d ( 𝑎 = ( 1st𝑧 ) → ( ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ↔ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ) )
61 60 rspcev ( ( ( 1st𝑧 ) ∈ 𝑅 ∧ ⟨ ( 1st𝑧 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ) → ∃ 𝑎 𝑅𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 )
62 55 58 61 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ∃ 𝑎 𝑅𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 )
63 rabn0 ( { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } ≠ ∅ ↔ ∃ 𝑎 𝑅𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 )
64 62 63 sylibr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } ≠ ∅ )
65 35 elin2d ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑥 ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) )
66 cnclima ( ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) ∈ ( 𝑅 Cn ( 𝑅 ×t 𝑆 ) ) ∧ 𝑥 ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) “ 𝑥 ) ∈ ( Clsd ‘ 𝑅 ) )
67 50 65 66 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑎 𝑅 ↦ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ) “ 𝑥 ) ∈ ( Clsd ‘ 𝑅 ) )
68 47 67 eqeltrrid ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } ∈ ( Clsd ‘ 𝑅 ) )
69 15 11 53 64 68 connclo ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } = 𝑅 )
70 31 69 eleqtrrd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 1st𝑤 ) ∈ { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } )
71 opeq1 ( 𝑎 = ( 1st𝑤 ) → ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ = ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ )
72 71 eleq1d ( 𝑎 = ( 1st𝑤 ) → ( ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ↔ ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ) )
73 72 elrab ( ( 1st𝑤 ) ∈ { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } ↔ ( ( 1st𝑤 ) ∈ 𝑅 ∧ ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ) )
74 73 simprbi ( ( 1st𝑤 ) ∈ { 𝑎 𝑅 ∣ ⟨ 𝑎 , ( 2nd𝑧 ) ⟩ ∈ 𝑥 } → ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 )
75 70 74 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 )
76 opeq2 ( 𝑎 = ( 2nd𝑧 ) → ⟨ ( 1st𝑤 ) , 𝑎 ⟩ = ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ )
77 76 eleq1d ( 𝑎 = ( 2nd𝑧 ) → ( ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 ↔ ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ) )
78 77 rspcev ( ( ( 2nd𝑧 ) ∈ 𝑆 ∧ ⟨ ( 1st𝑤 ) , ( 2nd𝑧 ) ⟩ ∈ 𝑥 ) → ∃ 𝑎 𝑆 ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 )
79 45 75 78 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ∃ 𝑎 𝑆 ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 )
80 rabn0 ( { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } ≠ ∅ ↔ ∃ 𝑎 𝑆 ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 )
81 79 80 sylibr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } ≠ ∅ )
82 cnclima ( ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) ∈ ( 𝑆 Cn ( 𝑅 ×t 𝑆 ) ) ∧ 𝑥 ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) “ 𝑥 ) ∈ ( Clsd ‘ 𝑆 ) )
83 34 65 82 syl2anc ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( ( 𝑎 𝑆 ↦ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ) “ 𝑥 ) ∈ ( Clsd ‘ 𝑆 ) )
84 25 83 eqeltrrid ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } ∈ ( Clsd ‘ 𝑆 ) )
85 16 13 39 81 84 connclo ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } = 𝑆 )
86 23 85 eleqtrrd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ( 2nd𝑤 ) ∈ { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } )
87 opeq2 ( 𝑎 = ( 2nd𝑤 ) → ⟨ ( 1st𝑤 ) , 𝑎 ⟩ = ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ )
88 87 eleq1d ( 𝑎 = ( 2nd𝑤 ) → ( ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 ↔ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ∈ 𝑥 ) )
89 88 elrab ( ( 2nd𝑤 ) ∈ { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } ↔ ( ( 2nd𝑤 ) ∈ 𝑆 ∧ ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ∈ 𝑥 ) )
90 89 simprbi ( ( 2nd𝑤 ) ∈ { 𝑎 𝑆 ∣ ⟨ ( 1st𝑤 ) , 𝑎 ⟩ ∈ 𝑥 } → ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ∈ 𝑥 )
91 86 90 syl ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → ⟨ ( 1st𝑤 ) , ( 2nd𝑤 ) ⟩ ∈ 𝑥 )
92 21 91 eqeltrd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ ( 𝑧𝑥𝑤 ( 𝑅 ×t 𝑆 ) ) ) → 𝑤𝑥 )
93 92 expr ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ 𝑧𝑥 ) → ( 𝑤 ( 𝑅 ×t 𝑆 ) → 𝑤𝑥 ) )
94 93 ssrdv ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ 𝑧𝑥 ) → ( 𝑅 ×t 𝑆 ) ⊆ 𝑥 )
95 9 94 eqssd ( ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) ∧ 𝑧𝑥 ) → 𝑥 = ( 𝑅 ×t 𝑆 ) )
96 95 ex ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) → ( 𝑧𝑥𝑥 = ( 𝑅 ×t 𝑆 ) ) )
97 96 exlimdv ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) → ( ∃ 𝑧 𝑧𝑥𝑥 = ( 𝑅 ×t 𝑆 ) ) )
98 5 97 syl5bi ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) → ( ¬ 𝑥 = ∅ → 𝑥 = ( 𝑅 ×t 𝑆 ) ) )
99 98 orrd ( ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) ∧ 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ) → ( 𝑥 = ∅ ∨ 𝑥 = ( 𝑅 ×t 𝑆 ) ) )
100 99 ex ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) → ( 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑥 = ∅ ∨ 𝑥 = ( 𝑅 ×t 𝑆 ) ) ) )
101 vex 𝑥 ∈ V
102 101 elpr ( 𝑥 ∈ { ∅ , ( 𝑅 ×t 𝑆 ) } ↔ ( 𝑥 = ∅ ∨ 𝑥 = ( 𝑅 ×t 𝑆 ) ) )
103 100 102 syl6ibr ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) → ( 𝑥 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) → 𝑥 ∈ { ∅ , ( 𝑅 ×t 𝑆 ) } ) )
104 103 ssrdv ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) → ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ⊆ { ∅ , ( 𝑅 ×t 𝑆 ) } )
105 eqid ( 𝑅 ×t 𝑆 ) = ( 𝑅 ×t 𝑆 )
106 105 isconn2 ( ( 𝑅 ×t 𝑆 ) ∈ Conn ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( ( 𝑅 ×t 𝑆 ) ∩ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ) ⊆ { ∅ , ( 𝑅 ×t 𝑆 ) } ) )
107 4 104 106 sylanbrc ( ( 𝑅 ∈ Conn ∧ 𝑆 ∈ Conn ) → ( 𝑅 ×t 𝑆 ) ∈ Conn )