| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | conntop 23426 | . . 3
⊢ (𝑅 ∈ Conn → 𝑅 ∈ Top) | 
| 2 |  | conntop 23426 | . . 3
⊢ (𝑆 ∈ Conn → 𝑆 ∈ Top) | 
| 3 |  | txtop 23578 | . . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) | 
| 4 | 1, 2, 3 | syl2an 596 | . 2
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Top) | 
| 5 |  | neq0 4351 | . . . . . . 7
⊢ (¬
𝑥 = ∅ ↔
∃𝑧 𝑧 ∈ 𝑥) | 
| 6 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) | 
| 7 | 6 | elin1d 4203 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆)) | 
| 8 |  | elssuni 4936 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑅 ×t 𝑆) → 𝑥 ⊆ ∪ (𝑅 ×t 𝑆)) | 
| 9 | 7, 8 | syl 17 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ∪ (𝑅 ×t 𝑆)) | 
| 10 |  | simprr 772 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 ∈ ∪ (𝑅 ×t 𝑆)) | 
| 11 |  | simplll 774 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑅 ∈ Conn) | 
| 12 | 11, 1 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑅 ∈ Top) | 
| 13 |  | simpllr 775 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑆 ∈ Conn) | 
| 14 | 13, 2 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑆 ∈ Top) | 
| 15 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑅 =
∪ 𝑅 | 
| 16 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑆 =
∪ 𝑆 | 
| 17 | 15, 16 | txuni 23601 | . . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) | 
| 18 | 12, 14, 17 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) | 
| 19 | 10, 18 | eleqtrrd 2843 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 ∈ (∪ 𝑅 × ∪ 𝑆)) | 
| 20 |  | 1st2nd2 8054 | . . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (∪ 𝑅
× ∪ 𝑆) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 21 | 19, 20 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) | 
| 22 |  | xp2nd 8048 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (∪ 𝑅
× ∪ 𝑆) → (2nd ‘𝑤) ∈ ∪ 𝑆) | 
| 23 | 19, 22 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (2nd
‘𝑤) ∈ ∪ 𝑆) | 
| 24 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ∪ 𝑆
↦ 〈(1st ‘𝑤), 𝑎〉) = (𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) | 
| 25 | 24 | mptpreima 6257 | . . . . . . . . . . . . . . . . 17
⊢ (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) = {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} | 
| 26 |  | toptopon2 22925 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆)) | 
| 27 | 14, 26 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘∪ 𝑆)) | 
| 28 |  | toptopon2 22925 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) | 
| 29 | 12, 28 | sylib 218 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘∪ 𝑅)) | 
| 30 |  | xp1st 8047 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (∪ 𝑅
× ∪ 𝑆) → (1st ‘𝑤) ∈ ∪ 𝑅) | 
| 31 | 19, 30 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (1st
‘𝑤) ∈ ∪ 𝑅) | 
| 32 | 27, 29, 31 | cnmptc 23671 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑆 ↦ (1st
‘𝑤)) ∈ (𝑆 Cn 𝑅)) | 
| 33 | 27 | cnmptid 23670 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑆 ↦ 𝑎) ∈ (𝑆 Cn 𝑆)) | 
| 34 | 27, 32, 33 | cnmpt1t 23674 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) ∈ (𝑆 Cn (𝑅 ×t 𝑆))) | 
| 35 |  | simplr 768 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) | 
| 36 | 35 | elin1d 4203 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆)) | 
| 37 |  | cnima 23274 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ∪ 𝑆
↦ 〈(1st ‘𝑤), 𝑎〉) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ 𝑆) | 
| 38 | 34, 36, 37 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ 𝑆) | 
| 39 | 25, 38 | eqeltrrid 2845 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ∈ 𝑆) | 
| 40 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 ∈ 𝑥) | 
| 41 |  | elunii 4911 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 ∈ ∪ (𝑅 ×t 𝑆)) | 
| 42 | 40, 36, 41 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 ∈ ∪ (𝑅 ×t 𝑆)) | 
| 43 | 42, 18 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 ∈ (∪ 𝑅 × ∪ 𝑆)) | 
| 44 |  | xp2nd 8048 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (∪ 𝑅
× ∪ 𝑆) → (2nd ‘𝑧) ∈ ∪ 𝑆) | 
| 45 | 43, 44 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (2nd
‘𝑧) ∈ ∪ 𝑆) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ∪ 𝑅
↦ 〈𝑎,
(2nd ‘𝑧)〉) = (𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) | 
| 47 | 46 | mptpreima 6257 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) = {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} | 
| 48 | 29 | cnmptid 23670 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑅 ↦ 𝑎) ∈ (𝑅 Cn 𝑅)) | 
| 49 | 29, 27, 45 | cnmptc 23671 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑅 ↦ (2nd
‘𝑧)) ∈ (𝑅 Cn 𝑆)) | 
| 50 | 29, 48, 49 | cnmpt1t 23674 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) ∈ (𝑅 Cn (𝑅 ×t 𝑆))) | 
| 51 |  | cnima 23274 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ∪ 𝑅
↦ 〈𝑎,
(2nd ‘𝑧)〉) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ 𝑅) | 
| 52 | 50, 36, 51 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ 𝑅) | 
| 53 | 47, 52 | eqeltrrid 2845 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ∈ 𝑅) | 
| 54 |  | xp1st 8047 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ (∪ 𝑅
× ∪ 𝑆) → (1st ‘𝑧) ∈ ∪ 𝑅) | 
| 55 | 43, 54 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (1st
‘𝑧) ∈ ∪ 𝑅) | 
| 56 |  | 1st2nd2 8054 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ (∪ 𝑅
× ∪ 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 57 | 43, 56 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 58 | 57, 40 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∈
𝑥) | 
| 59 |  | opeq1 4872 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = (1st ‘𝑧) → 〈𝑎, (2nd ‘𝑧)〉 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) | 
| 60 | 59 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = (1st ‘𝑧) → (〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥 ↔ 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∈
𝑥)) | 
| 61 | 60 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑧) ∈ ∪ 𝑅 ∧ 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∈
𝑥) → ∃𝑎 ∈ ∪ 𝑅〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥) | 
| 62 | 55, 58, 61 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → ∃𝑎 ∈ ∪ 𝑅〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥) | 
| 63 |  | rabn0 4388 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑎 ∈ ∪ 𝑅
∣ 〈𝑎,
(2nd ‘𝑧)〉 ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 ∈ ∪ 𝑅〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥) | 
| 64 | 62, 63 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ≠ ∅) | 
| 65 | 35 | elin2d 4204 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) | 
| 66 |  | cnclima 23277 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ∪ 𝑅
↦ 〈𝑎,
(2nd ‘𝑧)〉) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ (Clsd‘𝑅)) | 
| 67 | 50, 65, 66 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ (Clsd‘𝑅)) | 
| 68 | 47, 67 | eqeltrrid 2845 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ∈ (Clsd‘𝑅)) | 
| 69 | 15, 11, 53, 64, 68 | connclo 23424 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} = ∪
𝑅) | 
| 70 | 31, 69 | eleqtrrd 2843 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (1st
‘𝑤) ∈ {𝑎 ∈ ∪ 𝑅
∣ 〈𝑎,
(2nd ‘𝑧)〉 ∈ 𝑥}) | 
| 71 |  | opeq1 4872 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (1st ‘𝑤) → 〈𝑎, (2nd ‘𝑧)〉 = 〈(1st
‘𝑤), (2nd
‘𝑧)〉) | 
| 72 | 71 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (1st ‘𝑤) → (〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥 ↔ 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥)) | 
| 73 | 72 | elrab 3691 | . . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ↔ ((1st
‘𝑤) ∈ ∪ 𝑅
∧ 〈(1st ‘𝑤), (2nd ‘𝑧)〉 ∈ 𝑥)) | 
| 74 | 73 | simprbi 496 | . . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} → 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥) | 
| 75 | 70, 74 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥) | 
| 76 |  | opeq2 4873 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (2nd ‘𝑧) → 〈(1st
‘𝑤), 𝑎〉 = 〈(1st
‘𝑤), (2nd
‘𝑧)〉) | 
| 77 | 76 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (2nd ‘𝑧) → (〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥 ↔ 〈(1st ‘𝑤), (2nd ‘𝑧)〉 ∈ 𝑥)) | 
| 78 | 77 | rspcev 3621 | . . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑧) ∈ ∪ 𝑆 ∧ 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥) → ∃𝑎 ∈ ∪ 𝑆〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥) | 
| 79 | 45, 75, 78 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → ∃𝑎 ∈ ∪ 𝑆〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥) | 
| 80 |  | rabn0 4388 | . . . . . . . . . . . . . . . . 17
⊢ ({𝑎 ∈ ∪ 𝑆
∣ 〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 ∈ ∪ 𝑆〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥) | 
| 81 | 79, 80 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ≠ ∅) | 
| 82 |  | cnclima 23277 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ∪ 𝑆
↦ 〈(1st ‘𝑤), 𝑎〉) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ (Clsd‘𝑆)) | 
| 83 | 34, 65, 82 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ (Clsd‘𝑆)) | 
| 84 | 25, 83 | eqeltrrid 2845 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ∈ (Clsd‘𝑆)) | 
| 85 | 16, 13, 39, 81, 84 | connclo 23424 | . . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} = ∪ 𝑆) | 
| 86 | 23, 85 | eleqtrrd 2843 | . . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (2nd
‘𝑤) ∈ {𝑎 ∈ ∪ 𝑆
∣ 〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥}) | 
| 87 |  | opeq2 4873 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (2nd ‘𝑤) → 〈(1st
‘𝑤), 𝑎〉 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉) | 
| 88 | 87 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = (2nd ‘𝑤) → (〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥 ↔ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ 𝑥)) | 
| 89 | 88 | elrab 3691 | . . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ↔ ((2nd ‘𝑤) ∈ ∪ 𝑆
∧ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ 𝑥)) | 
| 90 | 89 | simprbi 496 | . . . . . . . . . . . . . 14
⊢
((2nd ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ 𝑥) | 
| 91 | 86, 90 | syl 17 | . . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 〈(1st
‘𝑤), (2nd
‘𝑤)〉 ∈
𝑥) | 
| 92 | 21, 91 | eqeltrd 2840 | . . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 ∈ 𝑥) | 
| 93 | 92 | expr 456 | . . . . . . . . . . 11
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → (𝑤 ∈ ∪ (𝑅 ×t 𝑆) → 𝑤 ∈ 𝑥)) | 
| 94 | 93 | ssrdv 3988 | . . . . . . . . . 10
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → ∪ (𝑅 ×t 𝑆) ⊆ 𝑥) | 
| 95 | 9, 94 | eqssd 4000 | . . . . . . . . 9
⊢ ((((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 = ∪ (𝑅 ×t 𝑆)) | 
| 96 | 95 | ex 412 | . . . . . . . 8
⊢ (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑧 ∈ 𝑥 → 𝑥 = ∪ (𝑅 ×t 𝑆))) | 
| 97 | 96 | exlimdv 1932 | . . . . . . 7
⊢ (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (∃𝑧 𝑧 ∈ 𝑥 → 𝑥 = ∪ (𝑅 ×t 𝑆))) | 
| 98 | 5, 97 | biimtrid 242 | . . . . . 6
⊢ (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (¬ 𝑥 = ∅ → 𝑥 = ∪ (𝑅 ×t 𝑆))) | 
| 99 | 98 | orrd 863 | . . . . 5
⊢ (((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = ∪ (𝑅 ×t 𝑆))) | 
| 100 | 99 | ex 412 | . . . 4
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = ∪ (𝑅 ×t 𝑆)))) | 
| 101 |  | vex 3483 | . . . . 5
⊢ 𝑥 ∈ V | 
| 102 | 101 | elpr 4649 | . . . 4
⊢ (𝑥 ∈ {∅, ∪ (𝑅
×t 𝑆)}
↔ (𝑥 = ∅ ∨
𝑥 = ∪ (𝑅
×t 𝑆))) | 
| 103 | 100, 102 | imbitrrdi 252 | . . 3
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, ∪ (𝑅
×t 𝑆)})) | 
| 104 | 103 | ssrdv 3988 | . 2
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, ∪ (𝑅
×t 𝑆)}) | 
| 105 |  | eqid 2736 | . . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) | 
| 106 | 105 | isconn2 23423 | . 2
⊢ ((𝑅 ×t 𝑆) ∈ Conn ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, ∪ (𝑅
×t 𝑆)})) | 
| 107 | 4, 104, 106 | sylanbrc 583 | 1
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn) |