Step | Hyp | Ref
| Expression |
1 | | topontop 20718 |
. . . . . 6
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top) |
2 | 1 | ad2antrr 762 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑅 ∈ Top) |
3 | | simprl 794 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ 𝑋) |
4 | | toponuni 20719 |
. . . . . . 7
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅) |
5 | 4 | ad2antrr 762 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑋 = ∪ 𝑅) |
6 | 3, 5 | sseqtrd 3641 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ∪ 𝑅) |
7 | | eqid 2622 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
8 | 7 | clscld 20851 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅)) |
9 | 2, 6, 8 | syl2anc 693 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅)) |
10 | | topontop 20718 |
. . . . . 6
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top) |
11 | 10 | ad2antlr 763 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑆 ∈ Top) |
12 | | simprr 796 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ 𝑌) |
13 | | toponuni 20719 |
. . . . . . 7
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑆) |
14 | 13 | ad2antlr 763 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑌 = ∪ 𝑆) |
15 | 12, 14 | sseqtrd 3641 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ∪ 𝑆) |
16 | | eqid 2622 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ 𝑆 |
17 | 16 | clscld 20851 |
. . . . 5
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) |
18 | 11, 15, 17 | syl2anc 693 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) |
19 | | txcld 21406 |
. . . 4
⊢
((((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅) ∧ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆))) |
20 | 9, 18, 19 | syl2anc 693 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆))) |
21 | 7 | sscls 20860 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ 𝐴 ⊆
((cls‘𝑅)‘𝐴)) |
22 | 2, 6, 21 | syl2anc 693 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴)) |
23 | 16 | sscls 20860 |
. . . . 5
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ 𝐵 ⊆
((cls‘𝑆)‘𝐵)) |
24 | 11, 15, 23 | syl2anc 693 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) |
25 | | xpss12 5225 |
. . . 4
⊢ ((𝐴 ⊆ ((cls‘𝑅)‘𝐴) ∧ 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
26 | 22, 24, 25 | syl2anc 693 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
27 | | eqid 2622 |
. . . 4
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
28 | 27 | clsss2 20876 |
. . 3
⊢
(((((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)) ∧ (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
29 | 20, 26, 28 | syl2anc 693 |
. 2
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
30 | | relxp 5227 |
. . . 4
⊢ Rel
(((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) |
31 | 30 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
32 | | opelxp 5146 |
. . . 4
⊢
(〈𝑥, 𝑦〉 ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ↔ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) |
33 | | eltx 21371 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
34 | 33 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
35 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (𝑟 × 𝑠) ↔ 〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠))) |
36 | 35 | anbi1d 741 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
37 | 36 | 2rexbidv 3057 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
38 | 37 | rspccva 3308 |
. . . . . . . . . 10
⊢
((∀𝑧 ∈
𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑢) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)) |
39 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑅 ∈ Top) |
40 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐴 ⊆ ∪ 𝑅) |
41 | | simplrl 800 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ ((cls‘𝑅)‘𝐴)) |
42 | | simprll 802 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑟 ∈ 𝑅) |
43 | | simprrl 804 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠)) |
44 | | opelxp 5146 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ↔ (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠)) |
45 | 43, 44 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠)) |
46 | 45 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ 𝑟) |
47 | 7 | clsndisj 20879 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅
∧ 𝑥 ∈
((cls‘𝑅)‘𝐴)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑥 ∈ 𝑟)) → (𝑟 ∩ 𝐴) ≠ ∅) |
48 | 39, 40, 41, 42, 46, 47 | syl32anc 1334 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 ∩ 𝐴) ≠ ∅) |
49 | | n0 3931 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∩ 𝐴) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴)) |
50 | 48, 49 | sylib 208 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴)) |
51 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑆 ∈ Top) |
52 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐵 ⊆ ∪ 𝑆) |
53 | | simplrr 801 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ ((cls‘𝑆)‘𝐵)) |
54 | | simprlr 803 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑠 ∈ 𝑆) |
55 | 45 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ 𝑠) |
56 | 16 | clsndisj 20879 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆
∧ 𝑦 ∈
((cls‘𝑆)‘𝐵)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ 𝑠)) → (𝑠 ∩ 𝐵) ≠ ∅) |
57 | 51, 52, 53, 54, 55, 56 | syl32anc 1334 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑠 ∩ 𝐵) ≠ ∅) |
58 | | n0 3931 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) |
59 | 57, 58 | sylib 208 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) |
60 | | eeanv 2182 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) ↔ (∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵))) |
61 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) ⊆ (𝑟 × 𝑠) |
62 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵))) |
63 | | inxp 5254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) = ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵)) |
64 | 62, 63 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵))) |
65 | 61, 64 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ (𝑟 × 𝑠)) |
66 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 × 𝑠) ⊆ 𝑢) |
67 | 66 | sselda 3603 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ 〈𝑧, 𝑤〉 ∈ (𝑟 × 𝑠)) → 〈𝑧, 𝑤〉 ∈ 𝑢) |
68 | 65, 67 | sylan2 491 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → 〈𝑧, 𝑤〉 ∈ 𝑢) |
69 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
70 | 69, 64 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) |
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) |
72 | | inelcm 4032 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑧, 𝑤〉 ∈ 𝑢 ∧ 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
73 | 68, 71, 72 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
74 | 73 | ex 450 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
75 | 74 | exlimdvv 1862 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
76 | 60, 75 | syl5bir 233 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
77 | 50, 59, 76 | mp2and 715 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
78 | 77 | expr 643 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
79 | 78 | rexlimdvva 3038 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
80 | 38, 79 | syl5 34 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ((∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
81 | 80 | expd 452 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
82 | 34, 81 | sylbid 230 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) → (〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
83 | 82 | ralrimiv 2965 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
84 | | txtopon 21394 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
85 | 84 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
86 | | topontop 20718 |
. . . . . . . 8
⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑅 ×t 𝑆) ∈ Top) |
87 | 85, 86 | syl 17 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ Top) |
88 | | xpss12 5225 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌)) |
89 | 88 | ad2antlr 763 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌)) |
90 | | toponuni 20719 |
. . . . . . . . 9
⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
91 | 85, 90 | syl 17 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
92 | 89, 91 | sseqtrd 3641 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆)) |
93 | 7 | clsss3 20863 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅) |
94 | 2, 6, 93 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅) |
95 | 94, 5 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ 𝑋) |
96 | 95 | sselda 3603 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑥 ∈ ((cls‘𝑅)‘𝐴)) → 𝑥 ∈ 𝑋) |
97 | 96 | adantrr 753 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑥 ∈ 𝑋) |
98 | 16 | clsss3 20863 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆) |
99 | 11, 15, 98 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆) |
100 | 99, 14 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ 𝑌) |
101 | 100 | sselda 3603 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 𝑦 ∈ 𝑌) |
102 | 101 | adantrl 752 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑦 ∈ 𝑌) |
103 | | opelxpi 5148 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
104 | 97, 102, 103 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
105 | 104, 91 | eleqtrd 2703 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ ∪
(𝑅 ×t
𝑆)) |
106 | 27 | elcls 20877 |
. . . . . . 7
⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆) ∧ 〈𝑥, 𝑦〉 ∈ ∪
(𝑅 ×t
𝑆)) → (〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
107 | 87, 92, 105, 106 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
108 | 83, 107 | mpbird 247 |
. . . . 5
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))) |
109 | 108 | ex 450 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))) |
110 | 32, 109 | syl5bi 232 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (〈𝑥, 𝑦〉 ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))) |
111 | 31, 110 | relssdv 5212 |
. 2
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ⊆ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))) |
112 | 29, 111 | eqssd 3620 |
1
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |