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

Theorem kqreglem2 23766
Description: If the Kolmogorov quotient of a space is regular then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
Assertion
Ref Expression
kqreglem2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem kqreglem2
Dummy variables 𝑚 𝑛 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 22935 . . 3 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
21adantr 480 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Top)
3 simplr 769 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → (KQ‘𝐽) ∈ Reg)
4 simpll 767 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → 𝐽 ∈ (TopOn‘𝑋))
5 simprl 771 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → 𝑧𝐽)
6 kqval.2 . . . . . . 7 𝐹 = (𝑥𝑋 ↦ {𝑦𝐽𝑥𝑦})
76kqopn 23758 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → (𝐹𝑧) ∈ (KQ‘𝐽))
84, 5, 7syl2anc 584 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → (𝐹𝑧) ∈ (KQ‘𝐽))
9 simprr 773 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → 𝑤𝑧)
10 toponss 22949 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → 𝑧𝑋)
114, 5, 10syl2anc 584 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → 𝑧𝑋)
1211, 9sseldd 3996 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → 𝑤𝑋)
136kqfvima 23754 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽𝑤𝑋) → (𝑤𝑧 ↔ (𝐹𝑤) ∈ (𝐹𝑧)))
144, 5, 12, 13syl3anc 1370 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → (𝑤𝑧 ↔ (𝐹𝑤) ∈ (𝐹𝑧)))
159, 14mpbid 232 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → (𝐹𝑤) ∈ (𝐹𝑧))
16 regsep 23358 . . . . 5 (((KQ‘𝐽) ∈ Reg ∧ (𝐹𝑧) ∈ (KQ‘𝐽) ∧ (𝐹𝑤) ∈ (𝐹𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))
173, 8, 15, 16syl3anc 1370 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → ∃𝑛 ∈ (KQ‘𝐽)((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))
184adantr 480 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝐽 ∈ (TopOn‘𝑋))
196kqid 23752 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
2018, 19syl 17 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽)))
21 simprl 771 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝑛 ∈ (KQ‘𝐽))
22 cnima 23289 . . . . . 6 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ 𝑛 ∈ (KQ‘𝐽)) → (𝐹𝑛) ∈ 𝐽)
2320, 21, 22syl2anc 584 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹𝑛) ∈ 𝐽)
2412adantr 480 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝑤𝑋)
25 simprrl 781 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹𝑤) ∈ 𝑛)
266kqffn 23749 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐹 Fn 𝑋)
27 elpreima 7078 . . . . . . 7 (𝐹 Fn 𝑋 → (𝑤 ∈ (𝐹𝑛) ↔ (𝑤𝑋 ∧ (𝐹𝑤) ∈ 𝑛)))
2818, 26, 273syl 18 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝑤 ∈ (𝐹𝑛) ↔ (𝑤𝑋 ∧ (𝐹𝑤) ∈ 𝑛)))
2924, 25, 28mpbir2and 713 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝑤 ∈ (𝐹𝑛))
306kqtopon 23751 . . . . . . . . . 10 (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹))
31 topontop 22935 . . . . . . . . . 10 ((KQ‘𝐽) ∈ (TopOn‘ran 𝐹) → (KQ‘𝐽) ∈ Top)
3218, 30, 313syl 18 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (KQ‘𝐽) ∈ Top)
33 elssuni 4942 . . . . . . . . . 10 (𝑛 ∈ (KQ‘𝐽) → 𝑛 (KQ‘𝐽))
3433ad2antrl 728 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝑛 (KQ‘𝐽))
35 eqid 2735 . . . . . . . . . 10 (KQ‘𝐽) = (KQ‘𝐽)
3635clscld 23071 . . . . . . . . 9 (((KQ‘𝐽) ∈ Top ∧ 𝑛 (KQ‘𝐽)) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
3732, 34, 36syl2anc 584 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽)))
38 cnclima 23292 . . . . . . . 8 ((𝐹 ∈ (𝐽 Cn (KQ‘𝐽)) ∧ ((cls‘(KQ‘𝐽))‘𝑛) ∈ (Clsd‘(KQ‘𝐽))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
3920, 37, 38syl2anc 584 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽))
4035sscls 23080 . . . . . . . . 9 (((KQ‘𝐽) ∈ Top ∧ 𝑛 (KQ‘𝐽)) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
4132, 34, 40syl2anc 584 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛))
42 imass2 6123 . . . . . . . 8 (𝑛 ⊆ ((cls‘(KQ‘𝐽))‘𝑛) → (𝐹𝑛) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
4341, 42syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹𝑛) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
44 eqid 2735 . . . . . . . 8 𝐽 = 𝐽
4544clsss2 23096 . . . . . . 7 (((𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ∈ (Clsd‘𝐽) ∧ (𝐹𝑛) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛))) → ((cls‘𝐽)‘(𝐹𝑛)) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
4639, 43, 45syl2anc 584 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘(𝐹𝑛)) ⊆ (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)))
47 simprrr 782 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧))
48 imass2 6123 . . . . . . . 8 (((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ (𝐹 “ (𝐹𝑧)))
4947, 48syl 17 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ (𝐹 “ (𝐹𝑧)))
505adantr 480 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → 𝑧𝐽)
516kqsat 23755 . . . . . . . 8 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑧𝐽) → (𝐹 “ (𝐹𝑧)) = 𝑧)
5218, 50, 51syl2anc 584 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹 “ (𝐹𝑧)) = 𝑧)
5349, 52sseqtrd 4036 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → (𝐹 “ ((cls‘(KQ‘𝐽))‘𝑛)) ⊆ 𝑧)
5446, 53sstrd 4006 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → ((cls‘𝐽)‘(𝐹𝑛)) ⊆ 𝑧)
55 eleq2 2828 . . . . . . 7 (𝑚 = (𝐹𝑛) → (𝑤𝑚𝑤 ∈ (𝐹𝑛)))
56 fveq2 6907 . . . . . . . 8 (𝑚 = (𝐹𝑛) → ((cls‘𝐽)‘𝑚) = ((cls‘𝐽)‘(𝐹𝑛)))
5756sseq1d 4027 . . . . . . 7 (𝑚 = (𝐹𝑛) → (((cls‘𝐽)‘𝑚) ⊆ 𝑧 ↔ ((cls‘𝐽)‘(𝐹𝑛)) ⊆ 𝑧))
5855, 57anbi12d 632 . . . . . 6 (𝑚 = (𝐹𝑛) → ((𝑤𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧) ↔ (𝑤 ∈ (𝐹𝑛) ∧ ((cls‘𝐽)‘(𝐹𝑛)) ⊆ 𝑧)))
5958rspcev 3622 . . . . 5 (((𝐹𝑛) ∈ 𝐽 ∧ (𝑤 ∈ (𝐹𝑛) ∧ ((cls‘𝐽)‘(𝐹𝑛)) ⊆ 𝑧)) → ∃𝑚𝐽 (𝑤𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
6023, 29, 54, 59syl12anc 837 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) ∧ (𝑛 ∈ (KQ‘𝐽) ∧ ((𝐹𝑤) ∈ 𝑛 ∧ ((cls‘(KQ‘𝐽))‘𝑛) ⊆ (𝐹𝑧)))) → ∃𝑚𝐽 (𝑤𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
6117, 60rexlimddv 3159 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) ∧ (𝑧𝐽𝑤𝑧)) → ∃𝑚𝐽 (𝑤𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
6261ralrimivva 3200 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → ∀𝑧𝐽𝑤𝑧𝑚𝐽 (𝑤𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧))
63 isreg 23356 . 2 (𝐽 ∈ Reg ↔ (𝐽 ∈ Top ∧ ∀𝑧𝐽𝑤𝑧𝑚𝐽 (𝑤𝑚 ∧ ((cls‘𝐽)‘𝑚) ⊆ 𝑧)))
642, 62, 63sylanbrc 583 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  wrex 3068  {crab 3433  wss 3963   cuni 4912  cmpt 5231  ccnv 5688  ran crn 5690  cima 5692   Fn wfn 6558  cfv 6563  (class class class)co 7431  Topctop 22915  TopOnctopon 22932  Clsdccld 23040  clsccl 23042   Cn ccn 23248  Regcreg 23333  KQckq 23717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8867  df-qtop 17554  df-top 22916  df-topon 22933  df-cld 23043  df-cls 23045  df-cn 23251  df-reg 23340  df-kq 23718
This theorem is referenced by:  kqreg  23775
  Copyright terms: Public domain W3C validator