| Step | Hyp | Ref
| Expression |
| 1 | | topontop 22919 |
. . . . . 6
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top) |
| 2 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑅 ∈ Top) |
| 3 | | simprl 771 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ 𝑋) |
| 4 | | toponuni 22920 |
. . . . . . 7
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅) |
| 5 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑋 = ∪ 𝑅) |
| 6 | 3, 5 | sseqtrd 4020 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ∪ 𝑅) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑅 =
∪ 𝑅 |
| 8 | 7 | clscld 23055 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅)) |
| 9 | 2, 6, 8 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅)) |
| 10 | | topontop 22919 |
. . . . . 6
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top) |
| 11 | 10 | ad2antlr 727 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑆 ∈ Top) |
| 12 | | simprr 773 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ 𝑌) |
| 13 | | toponuni 22920 |
. . . . . . 7
⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑆) |
| 14 | 13 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑌 = ∪ 𝑆) |
| 15 | 12, 14 | sseqtrd 4020 |
. . . . 5
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ∪ 𝑆) |
| 16 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑆 =
∪ 𝑆 |
| 17 | 16 | clscld 23055 |
. . . . 5
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) |
| 18 | 11, 15, 17 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) |
| 19 | | txcld 23611 |
. . . 4
⊢
((((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅) ∧ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆))) |
| 20 | 9, 18, 19 | syl2anc 584 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆))) |
| 21 | 7 | sscls 23064 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ 𝐴 ⊆
((cls‘𝑅)‘𝐴)) |
| 22 | 2, 6, 21 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴)) |
| 23 | 16 | sscls 23064 |
. . . . 5
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ 𝐵 ⊆
((cls‘𝑆)‘𝐵)) |
| 24 | 11, 15, 23 | syl2anc 584 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) |
| 25 | | xpss12 5700 |
. . . 4
⊢ ((𝐴 ⊆ ((cls‘𝑅)‘𝐴) ∧ 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
| 26 | 22, 24, 25 | syl2anc 584 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
| 27 | | eqid 2737 |
. . . 4
⊢ ∪ (𝑅
×t 𝑆) =
∪ (𝑅 ×t 𝑆) |
| 28 | 27 | clsss2 23080 |
. . 3
⊢
(((((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)) ∧ (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
| 29 | 20, 26, 28 | syl2anc 584 |
. 2
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
| 30 | | relxp 5703 |
. . . 4
⊢ Rel
(((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) |
| 31 | 30 | a1i 11 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |
| 32 | | opelxp 5721 |
. . . 4
⊢
(〈𝑥, 𝑦〉 ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ↔ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) |
| 33 | | eltx 23576 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
| 34 | 33 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
| 35 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑧 ∈ (𝑟 × 𝑠) ↔ 〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠))) |
| 36 | 35 | anbi1d 631 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
| 37 | 36 | 2rexbidv 3222 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) |
| 38 | 37 | rspccva 3621 |
. . . . . . . . . 10
⊢
((∀𝑧 ∈
𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑢) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)) |
| 39 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑅 ∈ Top) |
| 40 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐴 ⊆ ∪ 𝑅) |
| 41 | | simplrl 777 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ ((cls‘𝑅)‘𝐴)) |
| 42 | | simprll 779 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑟 ∈ 𝑅) |
| 43 | | simprrl 781 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠)) |
| 44 | | opelxp 5721 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ↔ (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠)) |
| 45 | 43, 44 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠)) |
| 46 | 45 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ 𝑟) |
| 47 | 7 | clsndisj 23083 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅
∧ 𝑥 ∈
((cls‘𝑅)‘𝐴)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑥 ∈ 𝑟)) → (𝑟 ∩ 𝐴) ≠ ∅) |
| 48 | 39, 40, 41, 42, 46, 47 | syl32anc 1380 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 ∩ 𝐴) ≠ ∅) |
| 49 | | n0 4353 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∩ 𝐴) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴)) |
| 50 | 48, 49 | sylib 218 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴)) |
| 51 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑆 ∈ Top) |
| 52 | 15 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐵 ⊆ ∪ 𝑆) |
| 53 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ ((cls‘𝑆)‘𝐵)) |
| 54 | | simprlr 780 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑠 ∈ 𝑆) |
| 55 | 45 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ 𝑠) |
| 56 | 16 | clsndisj 23083 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆
∧ 𝑦 ∈
((cls‘𝑆)‘𝐵)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ 𝑠)) → (𝑠 ∩ 𝐵) ≠ ∅) |
| 57 | 51, 52, 53, 54, 55, 56 | syl32anc 1380 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑠 ∩ 𝐵) ≠ ∅) |
| 58 | | n0 4353 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∩ 𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) |
| 59 | 57, 58 | sylib 218 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) |
| 60 | | exdistrv 1955 |
. . . . . . . . . . . . . 14
⊢
(∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) ↔ (∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵))) |
| 61 | | opelxpi 5722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵))) |
| 62 | | inxp 5842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) = ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵)) |
| 63 | 61, 62 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵))) |
| 64 | 63 | elin1d 4204 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ (𝑟 × 𝑠)) |
| 65 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 × 𝑠) ⊆ 𝑢) |
| 66 | 65 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ 〈𝑧, 𝑤〉 ∈ (𝑟 × 𝑠)) → 〈𝑧, 𝑤〉 ∈ 𝑢) |
| 67 | 64, 66 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → 〈𝑧, 𝑤〉 ∈ 𝑢) |
| 68 | 63 | elin2d 4205 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) |
| 70 | | inelcm 4465 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑧, 𝑤〉 ∈ 𝑢 ∧ 〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
| 71 | 67, 69, 70 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
| 72 | 71 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 73 | 72 | exlimdvv 1934 |
. . . . . . . . . . . . . 14
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 74 | 60, 73 | biimtrrid 243 |
. . . . . . . . . . . . 13
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 75 | 50, 59, 74 | mp2and 699 |
. . . . . . . . . . . 12
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅) |
| 76 | 75 | expr 456 |
. . . . . . . . . . 11
⊢
(((((𝑅 ∈
(TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 77 | 76 | rexlimdvva 3213 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (〈𝑥, 𝑦〉 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 78 | 38, 77 | syl5 34 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ((∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ 〈𝑥, 𝑦〉 ∈ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 79 | 78 | expd 415 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
| 80 | 34, 79 | sylbid 240 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) → (〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
| 81 | 80 | ralrimiv 3145 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)) |
| 82 | | txtopon 23599 |
. . . . . . . . 9
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 83 | 82 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) |
| 84 | | topontop 22919 |
. . . . . . . 8
⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑅 ×t 𝑆) ∈ Top) |
| 85 | 83, 84 | syl 17 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ Top) |
| 86 | | xpss12 5700 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌)) |
| 87 | 86 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌)) |
| 88 | | toponuni 22920 |
. . . . . . . . 9
⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
| 89 | 83, 88 | syl 17 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
| 90 | 87, 89 | sseqtrd 4020 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆)) |
| 91 | 7 | clsss3 23067 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅) |
| 92 | 2, 6, 91 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅) |
| 93 | 92, 5 | sseqtrrd 4021 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ 𝑋) |
| 94 | 93 | sselda 3983 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑥 ∈ ((cls‘𝑅)‘𝐴)) → 𝑥 ∈ 𝑋) |
| 95 | 94 | adantrr 717 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑥 ∈ 𝑋) |
| 96 | 16 | clsss3 23067 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆)
→ ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆) |
| 97 | 11, 15, 96 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆) |
| 98 | 97, 14 | sseqtrrd 4021 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ 𝑌) |
| 99 | 98 | sselda 3983 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 𝑦 ∈ 𝑌) |
| 100 | 99 | adantrl 716 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑦 ∈ 𝑌) |
| 101 | 95, 100 | opelxpd 5724 |
. . . . . . . 8
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ (𝑋 × 𝑌)) |
| 102 | 101, 89 | eleqtrd 2843 |
. . . . . . 7
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ ∪
(𝑅 ×t
𝑆)) |
| 103 | 27 | elcls 23081 |
. . . . . . 7
⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝐴 × 𝐵) ⊆ ∪
(𝑅 ×t
𝑆) ∧ 〈𝑥, 𝑦〉 ∈ ∪
(𝑅 ×t
𝑆)) → (〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
| 104 | 85, 90, 102, 103 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(〈𝑥, 𝑦〉 ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))) |
| 105 | 81, 104 | mpbird 257 |
. . . . 5
⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))) |
| 106 | 105 | ex 412 |
. . . 4
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))) |
| 107 | 32, 106 | biimtrid 242 |
. . 3
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (〈𝑥, 𝑦〉 ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) → 〈𝑥, 𝑦〉 ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))) |
| 108 | 31, 107 | relssdv 5798 |
. 2
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ⊆ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))) |
| 109 | 29, 108 | eqssd 4001 |
1
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) |