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 )