Step | Hyp | Ref
| Expression |
1 | | contop 21030 |
. . 3
⊢ (𝑅 ∈ Con → 𝑅 ∈ Top) |
2 | | contop 21030 |
. . 3
⊢ (𝑆 ∈ Con → 𝑆 ∈ Top) |
3 | | txtop 21182 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) |
4 | 1, 2, 3 | syl2an 493 |
. 2
⊢ ((𝑅 ∈ Con ∧ 𝑆 ∈ Con) → (𝑅 ×t 𝑆) ∈ Top) |
5 | | neq0 3889 |
. . . . . . 7
⊢ (¬
𝑥 = ∅ ↔
∃𝑧 𝑧 ∈ 𝑥) |
6 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ (𝑅 ×t 𝑆) |
7 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) |
8 | 6, 7 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 ∈ (𝑅 ×t 𝑆)) |
9 | | elssuni 4403 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑅 ×t 𝑆) → 𝑥 ⊆ ∪ (𝑅 ×t 𝑆)) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ∪ (𝑅 ×t 𝑆)) |
11 | | simprr 792 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 ∈ ∪ (𝑅 ×t 𝑆)) |
12 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑅 ∈ Con) |
13 | 12, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑅 ∈ Top) |
14 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑆 ∈ Con) |
15 | 14, 2 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑆 ∈ Top) |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑅 =
∪ 𝑅 |
17 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑆 =
∪ 𝑆 |
18 | 16, 17 | txuni 21205 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
19 | 13, 15, 18 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (∪ 𝑅
× ∪ 𝑆) = ∪ (𝑅 ×t 𝑆)) |
20 | 11, 19 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 ∈ (∪ 𝑅 × ∪ 𝑆)) |
21 | | 1st2nd2 7096 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ (∪ 𝑅
× ∪ 𝑆) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
23 | | xp2nd 7090 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (∪ 𝑅
× ∪ 𝑆) → (2nd ‘𝑤) ∈ ∪ 𝑆) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (2nd
‘𝑤) ∈ ∪ 𝑆) |
25 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ ∪ 𝑆
↦ 〈(1st ‘𝑤), 𝑎〉) = (𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) |
26 | 25 | mptpreima 5545 |
. . . . . . . . . . . . . . . . 17
⊢ (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) = {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} |
27 | 17 | toptopon 20548 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘∪ 𝑆)) |
28 | 15, 27 | sylib 207 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑆 ∈ (TopOn‘∪ 𝑆)) |
29 | 16 | toptopon 20548 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) |
30 | 13, 29 | sylib 207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑅 ∈ (TopOn‘∪ 𝑅)) |
31 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ (∪ 𝑅
× ∪ 𝑆) → (1st ‘𝑤) ∈ ∪ 𝑅) |
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (1st
‘𝑤) ∈ ∪ 𝑅) |
33 | 28, 30, 32 | cnmptc 21275 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑆 ↦ (1st
‘𝑤)) ∈ (𝑆 Cn 𝑅)) |
34 | 28 | cnmptid 21274 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑆 ↦ 𝑎) ∈ (𝑆 Cn 𝑆)) |
35 | 28, 33, 34 | cnmpt1t 21278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) ∈ (𝑆 Cn (𝑅 ×t 𝑆))) |
36 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) |
37 | 6, 36 | sseldi 3566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑥 ∈ (𝑅 ×t 𝑆)) |
38 | | cnima 20879 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ∪ 𝑆
↦ 〈(1st ‘𝑤), 𝑎〉) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ 𝑆) |
39 | 35, 37, 38 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ 𝑆) |
40 | 26, 39 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ∈ 𝑆) |
41 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 ∈ 𝑥) |
42 | | elunii 4377 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → 𝑧 ∈ ∪ (𝑅 ×t 𝑆)) |
43 | 41, 37, 42 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 ∈ ∪ (𝑅 ×t 𝑆)) |
44 | 43, 19 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 ∈ (∪ 𝑅 × ∪ 𝑆)) |
45 | | xp2nd 7090 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ (∪ 𝑅
× ∪ 𝑆) → (2nd ‘𝑧) ∈ ∪ 𝑆) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (2nd
‘𝑧) ∈ ∪ 𝑆) |
47 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 ∈ ∪ 𝑅
↦ 〈𝑎,
(2nd ‘𝑧)〉) = (𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) |
48 | 47 | mptpreima 5545 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) = {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} |
49 | 30 | cnmptid 21274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑅 ↦ 𝑎) ∈ (𝑅 Cn 𝑅)) |
50 | 30, 28, 46 | cnmptc 21275 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑅 ↦ (2nd
‘𝑧)) ∈ (𝑅 Cn 𝑆)) |
51 | 30, 49, 50 | cnmpt1t 21278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) ∈ (𝑅 Cn (𝑅 ×t 𝑆))) |
52 | | cnima 20879 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ∪ 𝑅
↦ 〈𝑎,
(2nd ‘𝑧)〉) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (𝑅 ×t 𝑆)) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ 𝑅) |
53 | 51, 37, 52 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ 𝑅) |
54 | 48, 53 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ∈ 𝑅) |
55 | | xp1st 7089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ (∪ 𝑅
× ∪ 𝑆) → (1st ‘𝑧) ∈ ∪ 𝑅) |
56 | 44, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (1st
‘𝑧) ∈ ∪ 𝑅) |
57 | | 1st2nd2 7096 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ (∪ 𝑅
× ∪ 𝑆) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
58 | 44, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
59 | 58, 41 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∈
𝑥) |
60 | | opeq1 4340 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = (1st ‘𝑧) → 〈𝑎, (2nd ‘𝑧)〉 = 〈(1st
‘𝑧), (2nd
‘𝑧)〉) |
61 | 60 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = (1st ‘𝑧) → (〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥 ↔ 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∈
𝑥)) |
62 | 61 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((1st ‘𝑧) ∈ ∪ 𝑅 ∧ 〈(1st
‘𝑧), (2nd
‘𝑧)〉 ∈
𝑥) → ∃𝑎 ∈ ∪ 𝑅〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥) |
63 | 56, 59, 62 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → ∃𝑎 ∈ ∪ 𝑅〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥) |
64 | | rabn0 3912 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑎 ∈ ∪ 𝑅
∣ 〈𝑎,
(2nd ‘𝑧)〉 ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 ∈ ∪ 𝑅〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥) |
65 | 63, 64 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ≠ ∅) |
66 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ (Clsd‘(𝑅 ×t 𝑆)) |
67 | 66, 36 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) |
68 | | cnclima 20882 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑎 ∈ ∪ 𝑅
↦ 〈𝑎,
(2nd ‘𝑧)〉) ∈ (𝑅 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ (Clsd‘𝑅)) |
69 | 51, 67, 68 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑅 ↦ 〈𝑎, (2nd ‘𝑧)〉) “ 𝑥) ∈ (Clsd‘𝑅)) |
70 | 48, 69 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ∈ (Clsd‘𝑅)) |
71 | 16, 12, 54, 65, 70 | conclo 21028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} = ∪
𝑅) |
72 | 32, 71 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (1st
‘𝑤) ∈ {𝑎 ∈ ∪ 𝑅
∣ 〈𝑎,
(2nd ‘𝑧)〉 ∈ 𝑥}) |
73 | | opeq1 4340 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (1st ‘𝑤) → 〈𝑎, (2nd ‘𝑧)〉 = 〈(1st
‘𝑤), (2nd
‘𝑧)〉) |
74 | 73 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (1st ‘𝑤) → (〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥 ↔ 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥)) |
75 | 74 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} ↔ ((1st
‘𝑤) ∈ ∪ 𝑅
∧ 〈(1st ‘𝑤), (2nd ‘𝑧)〉 ∈ 𝑥)) |
76 | 75 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑅 ∣ 〈𝑎, (2nd ‘𝑧)〉 ∈ 𝑥} → 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥) |
77 | 72, 76 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥) |
78 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = (2nd ‘𝑧) → 〈(1st
‘𝑤), 𝑎〉 = 〈(1st
‘𝑤), (2nd
‘𝑧)〉) |
79 | 78 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (2nd ‘𝑧) → (〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥 ↔ 〈(1st ‘𝑤), (2nd ‘𝑧)〉 ∈ 𝑥)) |
80 | 79 | rspcev 3282 |
. . . . . . . . . . . . . . . . . 18
⊢
(((2nd ‘𝑧) ∈ ∪ 𝑆 ∧ 〈(1st
‘𝑤), (2nd
‘𝑧)〉 ∈
𝑥) → ∃𝑎 ∈ ∪ 𝑆〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥) |
81 | 46, 77, 80 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → ∃𝑎 ∈ ∪ 𝑆〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥) |
82 | | rabn0 3912 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑎 ∈ ∪ 𝑆
∣ 〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥} ≠ ∅ ↔ ∃𝑎 ∈ ∪ 𝑆〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥) |
83 | 81, 82 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ≠ ∅) |
84 | | cnclima 20882 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑎 ∈ ∪ 𝑆
↦ 〈(1st ‘𝑤), 𝑎〉) ∈ (𝑆 Cn (𝑅 ×t 𝑆)) ∧ 𝑥 ∈ (Clsd‘(𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ (Clsd‘𝑆)) |
85 | 35, 67, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (◡(𝑎 ∈ ∪ 𝑆 ↦ 〈(1st
‘𝑤), 𝑎〉) “ 𝑥) ∈ (Clsd‘𝑆)) |
86 | 26, 85 | syl5eqelr 2693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ∈ (Clsd‘𝑆)) |
87 | 17, 14, 40, 83, 86 | conclo 21028 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} = ∪ 𝑆) |
88 | 24, 87 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → (2nd
‘𝑤) ∈ {𝑎 ∈ ∪ 𝑆
∣ 〈(1st ‘𝑤), 𝑎〉 ∈ 𝑥}) |
89 | | opeq2 4341 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (2nd ‘𝑤) → 〈(1st
‘𝑤), 𝑎〉 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉) |
90 | 89 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (2nd ‘𝑤) → (〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥 ↔ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ 𝑥)) |
91 | 90 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} ↔ ((2nd ‘𝑤) ∈ ∪ 𝑆
∧ 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ 𝑥)) |
92 | 91 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑤) ∈ {𝑎 ∈ ∪ 𝑆 ∣ 〈(1st
‘𝑤), 𝑎〉 ∈ 𝑥} → 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ∈ 𝑥) |
93 | 88, 92 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 〈(1st
‘𝑤), (2nd
‘𝑤)〉 ∈
𝑥) |
94 | 22, 93 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ ∪ (𝑅 ×t 𝑆))) → 𝑤 ∈ 𝑥) |
95 | 94 | expr 641 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → (𝑤 ∈ ∪ (𝑅 ×t 𝑆) → 𝑤 ∈ 𝑥)) |
96 | 95 | ssrdv 3574 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → ∪ (𝑅 ×t 𝑆) ⊆ 𝑥) |
97 | 10, 96 | eqssd 3585 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) ∧ 𝑧 ∈ 𝑥) → 𝑥 = ∪ (𝑅 ×t 𝑆)) |
98 | 97 | ex 449 |
. . . . . . . 8
⊢ (((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑧 ∈ 𝑥 → 𝑥 = ∪ (𝑅 ×t 𝑆))) |
99 | 98 | exlimdv 1848 |
. . . . . . 7
⊢ (((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (∃𝑧 𝑧 ∈ 𝑥 → 𝑥 = ∪ (𝑅 ×t 𝑆))) |
100 | 5, 99 | syl5bi 231 |
. . . . . 6
⊢ (((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (¬ 𝑥 = ∅ → 𝑥 = ∪ (𝑅 ×t 𝑆))) |
101 | 100 | orrd 392 |
. . . . 5
⊢ (((𝑅 ∈ Con ∧ 𝑆 ∈ Con) ∧ 𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆)))) → (𝑥 = ∅ ∨ 𝑥 = ∪ (𝑅 ×t 𝑆))) |
102 | 101 | ex 449 |
. . . 4
⊢ ((𝑅 ∈ Con ∧ 𝑆 ∈ Con) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → (𝑥 = ∅ ∨ 𝑥 = ∪ (𝑅 ×t 𝑆)))) |
103 | | vex 3176 |
. . . . 5
⊢ 𝑥 ∈ V |
104 | 103 | elpr 4146 |
. . . 4
⊢ (𝑥 ∈ {∅, ∪ (𝑅
×t 𝑆)}
↔ (𝑥 = ∅ ∨
𝑥 = ∪ (𝑅
×t 𝑆))) |
105 | 102, 104 | syl6ibr 241 |
. . 3
⊢ ((𝑅 ∈ Con ∧ 𝑆 ∈ Con) → (𝑥 ∈ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) → 𝑥 ∈ {∅, ∪ (𝑅
×t 𝑆)})) |
106 | 105 | ssrdv 3574 |
. 2
⊢ ((𝑅 ∈ Con ∧ 𝑆 ∈ Con) → ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, ∪ (𝑅
×t 𝑆)}) |
107 | | eqid 2610 |
. . 3
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
108 | 107 | iscon2 21027 |
. 2
⊢ ((𝑅 ×t 𝑆) ∈ Con ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ((𝑅 ×t 𝑆) ∩ (Clsd‘(𝑅 ×t 𝑆))) ⊆ {∅, ∪ (𝑅
×t 𝑆)})) |
109 | 4, 106, 108 | sylanbrc 695 |
1
⊢ ((𝑅 ∈ Con ∧ 𝑆 ∈ Con) → (𝑅 ×t 𝑆) ∈ Con) |