Step | Hyp | Ref
| Expression |
1 | | topontop 21088 |
. . . . . 6
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top) |
2 | 1 | ad2antrr 717 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑅 ∈ Top) |
3 | | simprl 787 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ 𝑋) |
4 | | toponuni 21089 |
. . . . . . 7
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅) |
5 | 4 | ad2antrr 717 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑋 = ∪ 𝑅) |
6 | 3, 5 | sseqtrd 3866 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ∪ 𝑅) |
7 | | eqid 2825 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
8 | 7 | clscld 21222 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅)) |
9 | 2, 6, 8 | syl2anc 579 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅)) |
10 | | topontop 21088 |
. . . . . 6
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top) |
11 | 10 | ad2antlr 718 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑆 ∈ Top) |
12 | | simprr 789 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ 𝑌) |
13 | | toponuni 21089 |
. . . . . . 7
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑆) |
14 | 13 | ad2antlr 718 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑌 = ∪ 𝑆) |
15 | 12, 14 | sseqtrd 3866 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ∪ 𝑆) |
16 | | eqid 2825 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ 𝑆 |
17 | 16 | clscld 21222 |
. . . . 5
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) |
18 | 11, 15, 17 | syl2anc 579 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) |
19 | | txcld 21777 |
. . . 4
⊢
((((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅) ∧ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆))) |
20 | 9, 18, 19 | syl2anc 579 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆))) |
21 | 7 | sscls 21231 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ 𝐴 ⊆
((cls‘𝑅)‘𝐴)) |
22 | 2, 6, 21 | syl2anc 579 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴)) |
23 | 16 | sscls 21231 |
. . . . 5
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ 𝐵 ⊆
((cls‘𝑆)‘𝐵)) |
24 | 11, 15, 23 | syl2anc 579 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) |
25 | | xpss12 5357 |
. . . 4
⊢ ((𝐴 ⊆ ((cls‘𝑅)‘𝐴) ∧ 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
26 | 22, 24, 25 | syl2anc 579 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
27 | | eqid 2825 |
. . . 4
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
28 | 27 | clsss2 21247 |
. . 3
⊢
(((((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)) ∧ (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
29 | 20, 26, 28 | syl2anc 579 |
. 2
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
30 | | relxp 5360 |
. . . 4
⊢ Rel
(((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) |
31 | 30 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
32 | | opelxp 5378 |
. . . 4
⊢
(〈𝑥, 𝑦〉 ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ↔ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) |
33 | | eltx 21742 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
34 | 33 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
35 | | eleq1 2894 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (𝑟 × 𝑠) ↔ 〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠))) |
36 | 35 | anbi1d 623 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
37 | 36 | 2rexbidv 3267 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
38 | 37 | rspccva 3525 |
. . . . . . . . . 10
⊢
((∀𝑧 ∈
𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑢) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)) |
39 | 2 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑅 ∈ Top) |
40 | 6 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐴 ⊆ ∪ 𝑅) |
41 | | simplrl 795 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ ((cls‘𝑅)‘𝐴)) |
42 | | simprll 797 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑟 ∈ 𝑅) |
43 | | simprrl 799 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠)) |
44 | | opelxp 5378 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ↔ (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠)) |
45 | 43, 44 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠)) |
46 | 45 | simpld 490 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ 𝑟) |
47 | 7 | clsndisj 21250 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅
∧ 𝑥 ∈
((cls‘𝑅)‘𝐴)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑥 ∈ 𝑟)) → (𝑟 ∩ 𝐴) ≠ ∅) |
48 | 39, 40, 41, 42, 46, 47 | syl32anc 1501 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 ∩ 𝐴) ≠ ∅) |
49 | | n0 4160 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∩ 𝐴) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴)) |
50 | 48, 49 | sylib 210 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴)) |
51 | 11 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑆 ∈ Top) |
52 | 15 | ad2antrr 717 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐵 ⊆ ∪ 𝑆) |
53 | | simplrr 796 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ ((cls‘𝑆)‘𝐵)) |
54 | | simprlr 798 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑠 ∈ 𝑆) |
55 | 45 | simprd 491 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ 𝑠) |
56 | 16 | clsndisj 21250 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆
∧ 𝑦 ∈
((cls‘𝑆)‘𝐵)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ 𝑠)) → (𝑠 ∩ 𝐵) ≠ ∅) |
57 | 51, 52, 53, 54, 55, 56 | syl32anc 1501 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑠 ∩ 𝐵) ≠ ∅) |
58 | | n0 4160 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) |
59 | 57, 58 | sylib 210 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) |
60 | | exdistrv 2054 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) ↔ (∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵))) |
61 | | inss1 4057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) ⊆ (𝑟 × 𝑠) |
62 | | opelxpi 5379 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵))) |
63 | | inxp 5487 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) = ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵)) |
64 | 62, 63 | syl6eleqr 2917 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵))) |
65 | 61, 64 | sseldi 3825 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ (𝑟 × 𝑠)) |
66 | | simprrr 800 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 × 𝑠) ⊆ 𝑢) |
67 | 66 | sselda 3827 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ 〈𝑧, 𝑤〉 ∈ (𝑟 × 𝑠)) → 〈𝑧, 𝑤〉 ∈ 𝑢) |
68 | 65, 67 | sylan2 586 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → 〈𝑧, 𝑤〉 ∈ 𝑢) |
69 | | inss2 4058 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
70 | 69, 64 | sseldi 3825 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) |
71 | 70 | adantl 475 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) |
72 | | inelcm 4256 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑧, 𝑤〉 ∈ 𝑢 ∧ 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
73 | 68, 71, 72 | syl2anc 579 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
74 | 73 | ex 403 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
75 | 74 | exlimdvv 2033 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
76 | 60, 75 | syl5bir 235 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
77 | 50, 59, 76 | mp2and 690 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
78 | 77 | expr 450 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
79 | 78 | rexlimdvva 3248 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
80 | 38, 79 | syl5 34 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ((∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
81 | 80 | expd 406 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
82 | 34, 81 | sylbid 232 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) → (〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
83 | 82 | ralrimiv 3174 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
84 | | txtopon 21765 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
85 | 84 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
86 | | topontop 21088 |
. . . . . . . 8
⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑅 ×t 𝑆) ∈ Top) |
87 | 85, 86 | syl 17 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ Top) |
88 | | xpss12 5357 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌)) |
89 | 88 | ad2antlr 718 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌)) |
90 | | toponuni 21089 |
. . . . . . . . 9
⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
91 | 85, 90 | syl 17 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
92 | 89, 91 | sseqtrd 3866 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆)) |
93 | 7 | clsss3 21234 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅) |
94 | 2, 6, 93 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅) |
95 | 94, 5 | sseqtr4d 3867 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ 𝑋) |
96 | 95 | sselda 3827 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑥 ∈ ((cls‘𝑅)‘𝐴)) → 𝑥 ∈ 𝑋) |
97 | 96 | adantrr 708 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑥 ∈ 𝑋) |
98 | 16 | clsss3 21234 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆) |
99 | 11, 15, 98 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆) |
100 | 99, 14 | sseqtr4d 3867 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ 𝑌) |
101 | 100 | sselda 3827 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 𝑦 ∈ 𝑌) |
102 | 101 | adantrl 707 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑦 ∈ 𝑌) |
103 | | opelxpi 5379 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
104 | 97, 102, 103 | syl2anc 579 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
105 | 104, 91 | eleqtrd 2908 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ ∪
(𝑅 ×t
𝑆)) |
106 | 27 | elcls 21248 |
. . . . . . 7
⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆) ∧ 〈𝑥, 𝑦〉 ∈ ∪
(𝑅 ×t
𝑆)) → (〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
107 | 87, 92, 105, 106 | syl3anc 1494 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
108 | 83, 107 | mpbird 249 |
. . . . 5
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))) |
109 | 108 | ex 403 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))) |
110 | 32, 109 | syl5bi 234 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (〈𝑥, 𝑦〉 ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))) |
111 | 31, 110 | relssdv 5446 |
. 2
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ⊆ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))) |
112 | 29, 111 | eqssd 3844 |
1
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |