MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txcls Structured version   Visualization version   GIF version

Theorem txcls 23521
Description: Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.)
Assertion
Ref Expression
txcls (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))

Proof of Theorem txcls
Dummy variables 𝑠 𝑟 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 22828 . . . . . 6 (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top)
21ad2antrr 725 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝑅 ∈ Top)
3 simprl 770 . . . . . 6 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝐴𝑋)
4 toponuni 22829 . . . . . . 7 (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = 𝑅)
54ad2antrr 725 . . . . . 6 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝑋 = 𝑅)
63, 5sseqtrd 4020 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝐴 𝑅)
7 eqid 2728 . . . . . 6 𝑅 = 𝑅
87clscld 22964 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴 𝑅) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅))
92, 6, 8syl2anc 583 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅))
10 topontop 22828 . . . . . 6 (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top)
1110ad2antlr 726 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝑆 ∈ Top)
12 simprr 772 . . . . . 6 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝐵𝑌)
13 toponuni 22829 . . . . . . 7 (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = 𝑆)
1413ad2antlr 726 . . . . . 6 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝑌 = 𝑆)
1512, 14sseqtrd 4020 . . . . 5 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝐵 𝑆)
16 eqid 2728 . . . . . 6 𝑆 = 𝑆
1716clscld 22964 . . . . 5 ((𝑆 ∈ Top ∧ 𝐵 𝑆) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆))
1811, 15, 17syl2anc 583 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆))
19 txcld 23520 . . . 4 ((((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅) ∧ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)))
209, 18, 19syl2anc 583 . . 3 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)))
217sscls 22973 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴 𝑅) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴))
222, 6, 21syl2anc 583 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴))
2316sscls 22973 . . . . 5 ((𝑆 ∈ Top ∧ 𝐵 𝑆) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵))
2411, 15, 23syl2anc 583 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵))
25 xpss12 5693 . . . 4 ((𝐴 ⊆ ((cls‘𝑅)‘𝐴) ∧ 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
2622, 24, 25syl2anc 583 . . 3 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
27 eqid 2728 . . . 4 (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
2827clsss2 22989 . . 3 (((((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)) ∧ (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
2920, 26, 28syl2anc 583 . 2 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
30 relxp 5696 . . . 4 Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))
3130a1i 11 . . 3 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
32 opelxp 5714 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ↔ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)))
33 eltx 23485 . . . . . . . . 9 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧𝑢𝑟𝑅𝑠𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
3433ad2antrr 725 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧𝑢𝑟𝑅𝑠𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
35 eleq1 2817 . . . . . . . . . . . . 13 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ (𝑟 × 𝑠) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠)))
3635anbi1d 630 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
37362rexbidv 3216 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑟𝑅𝑠𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ ∃𝑟𝑅𝑠𝑆 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
3837rspccva 3608 . . . . . . . . . 10 ((∀𝑧𝑢𝑟𝑅𝑠𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑢) → ∃𝑟𝑅𝑠𝑆 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))
392ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑅 ∈ Top)
406ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐴 𝑅)
41 simplrl 776 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ ((cls‘𝑅)‘𝐴))
42 simprll 778 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑟𝑅)
43 simprrl 780 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠))
44 opelxp 5714 . . . . . . . . . . . . . . . . 17 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ↔ (𝑥𝑟𝑦𝑠))
4543, 44sylib 217 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑥𝑟𝑦𝑠))
4645simpld 494 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥𝑟)
477clsndisj 22992 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝐴 𝑅𝑥 ∈ ((cls‘𝑅)‘𝐴)) ∧ (𝑟𝑅𝑥𝑟)) → (𝑟𝐴) ≠ ∅)
4839, 40, 41, 42, 46, 47syl32anc 1376 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟𝐴) ≠ ∅)
49 n0 4347 . . . . . . . . . . . . . 14 ((𝑟𝐴) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑟𝐴))
5048, 49sylib 217 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑧 𝑧 ∈ (𝑟𝐴))
5111ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑆 ∈ Top)
5215ad2antrr 725 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐵 𝑆)
53 simplrr 777 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ ((cls‘𝑆)‘𝐵))
54 simprlr 779 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑠𝑆)
5545simprd 495 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦𝑠)
5616clsndisj 22992 . . . . . . . . . . . . . . 15 (((𝑆 ∈ Top ∧ 𝐵 𝑆𝑦 ∈ ((cls‘𝑆)‘𝐵)) ∧ (𝑠𝑆𝑦𝑠)) → (𝑠𝐵) ≠ ∅)
5751, 52, 53, 54, 55, 56syl32anc 1376 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑠𝐵) ≠ ∅)
58 n0 4347 . . . . . . . . . . . . . 14 ((𝑠𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑠𝐵))
5957, 58sylib 217 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑤 𝑤 ∈ (𝑠𝐵))
60 exdistrv 1952 . . . . . . . . . . . . . 14 (∃𝑧𝑤(𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) ↔ (∃𝑧 𝑧 ∈ (𝑟𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠𝐵)))
61 opelxpi 5715 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) → ⟨𝑧, 𝑤⟩ ∈ ((𝑟𝐴) × (𝑠𝐵)))
62 inxp 5834 . . . . . . . . . . . . . . . . . . . 20 ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) = ((𝑟𝐴) × (𝑠𝐵))
6361, 62eleqtrrdi 2840 . . . . . . . . . . . . . . . . . . 19 ((𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) → ⟨𝑧, 𝑤⟩ ∈ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)))
6463elin1d 4198 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) → ⟨𝑧, 𝑤⟩ ∈ (𝑟 × 𝑠))
65 simprrr 781 . . . . . . . . . . . . . . . . . . 19 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 × 𝑠) ⊆ 𝑢)
6665sselda 3980 . . . . . . . . . . . . . . . . . 18 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑟 × 𝑠)) → ⟨𝑧, 𝑤⟩ ∈ 𝑢)
6764, 66sylan2 592 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵))) → ⟨𝑧, 𝑤⟩ ∈ 𝑢)
6863elin2d 4199 . . . . . . . . . . . . . . . . . 18 ((𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) → ⟨𝑧, 𝑤⟩ ∈ (𝐴 × 𝐵))
6968adantl 481 . . . . . . . . . . . . . . . . 17 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵))) → ⟨𝑧, 𝑤⟩ ∈ (𝐴 × 𝐵))
70 inelcm 4465 . . . . . . . . . . . . . . . . 17 ((⟨𝑧, 𝑤⟩ ∈ 𝑢 ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐴 × 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)
7167, 69, 70syl2anc 583 . . . . . . . . . . . . . . . 16 ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)
7271ex 412 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
7372exlimdvv 1930 . . . . . . . . . . . . . 14 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (∃𝑧𝑤(𝑧 ∈ (𝑟𝐴) ∧ 𝑤 ∈ (𝑠𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
7460, 73biimtrrid 242 . . . . . . . . . . . . 13 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((∃𝑧 𝑧 ∈ (𝑟𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
7550, 59, 74mp2and 698 . . . . . . . . . . . 12 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟𝑅𝑠𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)
7675expr 456 . . . . . . . . . . 11 (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ (𝑟𝑅𝑠𝑆)) → ((⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
7776rexlimdvva 3208 . . . . . . . . . 10 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∃𝑟𝑅𝑠𝑆 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
7838, 77syl5 34 . . . . . . . . 9 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ((∀𝑧𝑢𝑟𝑅𝑠𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
7978expd 415 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∀𝑧𝑢𝑟𝑅𝑠𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
8034, 79sylbid 239 . . . . . . 7 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) → (⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
8180ralrimiv 3142 . . . . . 6 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ∀𝑢 ∈ (𝑅 ×t 𝑆)(⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
82 txtopon 23508 . . . . . . . . 9 ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)))
8382ad2antrr 725 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)))
84 topontop 22828 . . . . . . . 8 ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑅 ×t 𝑆) ∈ Top)
8583, 84syl 17 . . . . . . 7 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ Top)
86 xpss12 5693 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
8786ad2antlr 726 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
88 toponuni 22829 . . . . . . . . 9 ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = (𝑅 ×t 𝑆))
8983, 88syl 17 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑋 × 𝑌) = (𝑅 ×t 𝑆))
9087, 89sseqtrd 4020 . . . . . . 7 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ (𝑅 ×t 𝑆))
917clsss3 22976 . . . . . . . . . . . . 13 ((𝑅 ∈ Top ∧ 𝐴 𝑅) → ((cls‘𝑅)‘𝐴) ⊆ 𝑅)
922, 6, 91syl2anc 583 . . . . . . . . . . . 12 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ 𝑅)
9392, 5sseqtrrd 4021 . . . . . . . . . . 11 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ 𝑋)
9493sselda 3980 . . . . . . . . . 10 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ 𝑥 ∈ ((cls‘𝑅)‘𝐴)) → 𝑥𝑋)
9594adantrr 716 . . . . . . . . 9 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑥𝑋)
9616clsss3 22976 . . . . . . . . . . . . 13 ((𝑆 ∈ Top ∧ 𝐵 𝑆) → ((cls‘𝑆)‘𝐵) ⊆ 𝑆)
9711, 15, 96syl2anc 583 . . . . . . . . . . . 12 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ 𝑆)
9897, 14sseqtrrd 4021 . . . . . . . . . . 11 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ 𝑌)
9998sselda 3980 . . . . . . . . . 10 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 𝑦𝑌)
10099adantrl 715 . . . . . . . . 9 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑦𝑌)
10195, 100opelxpd 5717 . . . . . . . 8 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
102101, 89eleqtrd 2831 . . . . . . 7 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ⟨𝑥, 𝑦⟩ ∈ (𝑅 ×t 𝑆))
10327elcls 22990 . . . . . . 7 (((𝑅 ×t 𝑆) ∈ Top ∧ (𝐴 × 𝐵) ⊆ (𝑅 ×t 𝑆) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝑅 ×t 𝑆)) → (⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
10485, 90, 102, 103syl3anc 1369 . . . . . 6 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
10581, 104mpbird 257 . . . . 5 ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))
106105ex 412 . . . 4 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))))
10732, 106biimtrid 241 . . 3 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → (⟨𝑥, 𝑦⟩ ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))))
10831, 107relssdv 5790 . 2 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ⊆ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))
10929, 108eqssd 3997 1 (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴𝑋𝐵𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1534  wex 1774  wcel 2099  wne 2937  wral 3058  wrex 3067  cin 3946  wss 3947  c0 4323  cop 4635   cuni 4908   × cxp 5676  Rel wrel 5683  cfv 6548  (class class class)co 7420  Topctop 22808  TopOnctopon 22825  Clsdccld 22933  clsccl 22935   ×t ctx 23477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 7993  df-2nd 7994  df-topgen 17425  df-top 22809  df-topon 22826  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-tx 23479
This theorem is referenced by:  clssubg  24026
  Copyright terms: Public domain W3C validator