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

Theorem fclscmp 23754
Description: A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Assertion
Ref Expression
fclscmp (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (𝐽 ∈ Comp ↔ βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ…))
Distinct variable groups:   𝑓,𝐽   𝑓,𝑋

Proof of Theorem fclscmp
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2730 . . . . 5 βˆͺ 𝐽 = βˆͺ 𝐽
21fclscmpi 23753 . . . 4 ((𝐽 ∈ Comp ∧ 𝑓 ∈ (Filβ€˜βˆͺ 𝐽)) β†’ (𝐽 fClus 𝑓) β‰  βˆ…)
32ralrimiva 3144 . . 3 (𝐽 ∈ Comp β†’ βˆ€π‘“ ∈ (Filβ€˜βˆͺ 𝐽)(𝐽 fClus 𝑓) β‰  βˆ…)
4 toponuni 22636 . . . . 5 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
54fveq2d 6894 . . . 4 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (Filβ€˜π‘‹) = (Filβ€˜βˆͺ 𝐽))
65raleqdv 3323 . . 3 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… ↔ βˆ€π‘“ ∈ (Filβ€˜βˆͺ 𝐽)(𝐽 fClus 𝑓) β‰  βˆ…))
73, 6imbitrrid 245 . 2 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (𝐽 ∈ Comp β†’ βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ…))
8 elpwi 4608 . . . . . 6 (π‘₯ ∈ 𝒫 (Clsdβ€˜π½) β†’ π‘₯ βŠ† (Clsdβ€˜π½))
9 vn0 4337 . . . . . . . . . 10 V β‰  βˆ…
10 simpr 483 . . . . . . . . . . . . 13 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ = βˆ…) β†’ π‘₯ = βˆ…)
1110inteqd 4954 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ = βˆ…) β†’ ∩ π‘₯ = ∩ βˆ…)
12 int0 4965 . . . . . . . . . . . 12 ∩ βˆ… = V
1311, 12eqtrdi 2786 . . . . . . . . . . 11 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ = βˆ…) β†’ ∩ π‘₯ = V)
1413neeq1d 2998 . . . . . . . . . 10 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ = βˆ…) β†’ (∩ π‘₯ β‰  βˆ… ↔ V β‰  βˆ…))
159, 14mpbiri 257 . . . . . . . . 9 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ = βˆ…) β†’ ∩ π‘₯ β‰  βˆ…)
1615a1d 25 . . . . . . . 8 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ = βˆ…) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ ∩ π‘₯ β‰  βˆ…))
17 ssfii 9416 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ V β†’ π‘₯ βŠ† (fiβ€˜π‘₯))
1817elv 3478 . . . . . . . . . . . . . . 15 π‘₯ βŠ† (fiβ€˜π‘₯)
19 simplrl 773 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ π‘₯ βŠ† (Clsdβ€˜π½))
201cldss2 22754 . . . . . . . . . . . . . . . . . . 19 (Clsdβ€˜π½) βŠ† 𝒫 βˆͺ 𝐽
214ad2antrr 722 . . . . . . . . . . . . . . . . . . . 20 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ 𝑋 = βˆͺ 𝐽)
2221pweqd 4618 . . . . . . . . . . . . . . . . . . 19 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ 𝒫 𝑋 = 𝒫 βˆͺ 𝐽)
2320, 22sseqtrrid 4034 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ (Clsdβ€˜π½) βŠ† 𝒫 𝑋)
2419, 23sstrd 3991 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ π‘₯ βŠ† 𝒫 𝑋)
25 simpr 483 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ π‘₯ β‰  βˆ…)
26 simplrr 774 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ Β¬ βˆ… ∈ (fiβ€˜π‘₯))
27 toponmax 22648 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 ∈ 𝐽)
2827ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ 𝑋 ∈ 𝐽)
29 fsubbas 23591 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ 𝐽 β†’ ((fiβ€˜π‘₯) ∈ (fBasβ€˜π‘‹) ↔ (π‘₯ βŠ† 𝒫 𝑋 ∧ π‘₯ β‰  βˆ… ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))))
3028, 29syl 17 . . . . . . . . . . . . . . . . 17 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ ((fiβ€˜π‘₯) ∈ (fBasβ€˜π‘‹) ↔ (π‘₯ βŠ† 𝒫 𝑋 ∧ π‘₯ β‰  βˆ… ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))))
3124, 25, 26, 30mpbir3and 1340 . . . . . . . . . . . . . . . 16 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ (fiβ€˜π‘₯) ∈ (fBasβ€˜π‘‹))
32 ssfg 23596 . . . . . . . . . . . . . . . 16 ((fiβ€˜π‘₯) ∈ (fBasβ€˜π‘‹) β†’ (fiβ€˜π‘₯) βŠ† (𝑋filGen(fiβ€˜π‘₯)))
3331, 32syl 17 . . . . . . . . . . . . . . 15 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ (fiβ€˜π‘₯) βŠ† (𝑋filGen(fiβ€˜π‘₯)))
3418, 33sstrid 3992 . . . . . . . . . . . . . 14 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ π‘₯ βŠ† (𝑋filGen(fiβ€˜π‘₯)))
3534sselda 3981 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ (𝑋filGen(fiβ€˜π‘₯)))
36 fclssscls 23742 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑋filGen(fiβ€˜π‘₯)) β†’ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† ((clsβ€˜π½)β€˜π‘¦))
3735, 36syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) ∧ 𝑦 ∈ π‘₯) β†’ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† ((clsβ€˜π½)β€˜π‘¦))
3819sselda 3981 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ (Clsdβ€˜π½))
39 cldcls 22766 . . . . . . . . . . . . 13 (𝑦 ∈ (Clsdβ€˜π½) β†’ ((clsβ€˜π½)β€˜π‘¦) = 𝑦)
4038, 39syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) ∧ 𝑦 ∈ π‘₯) β†’ ((clsβ€˜π½)β€˜π‘¦) = 𝑦)
4137, 40sseqtrd 4021 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) ∧ 𝑦 ∈ π‘₯) β†’ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† 𝑦)
4241ralrimiva 3144 . . . . . . . . . 10 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ βˆ€π‘¦ ∈ π‘₯ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† 𝑦)
43 ssint 4967 . . . . . . . . . 10 ((𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† ∩ π‘₯ ↔ βˆ€π‘¦ ∈ π‘₯ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† 𝑦)
4442, 43sylibr 233 . . . . . . . . 9 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† ∩ π‘₯)
45 fgcl 23602 . . . . . . . . . 10 ((fiβ€˜π‘₯) ∈ (fBasβ€˜π‘‹) β†’ (𝑋filGen(fiβ€˜π‘₯)) ∈ (Filβ€˜π‘‹))
46 oveq2 7419 . . . . . . . . . . . 12 (𝑓 = (𝑋filGen(fiβ€˜π‘₯)) β†’ (𝐽 fClus 𝑓) = (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))))
4746neeq1d 2998 . . . . . . . . . . 11 (𝑓 = (𝑋filGen(fiβ€˜π‘₯)) β†’ ((𝐽 fClus 𝑓) β‰  βˆ… ↔ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) β‰  βˆ…))
4847rspcv 3607 . . . . . . . . . 10 ((𝑋filGen(fiβ€˜π‘₯)) ∈ (Filβ€˜π‘‹) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) β‰  βˆ…))
4931, 45, 483syl 18 . . . . . . . . 9 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) β‰  βˆ…))
50 ssn0 4399 . . . . . . . . 9 (((𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) βŠ† ∩ π‘₯ ∧ (𝐽 fClus (𝑋filGen(fiβ€˜π‘₯))) β‰  βˆ…) β†’ ∩ π‘₯ β‰  βˆ…)
5144, 49, 50syl6an 680 . . . . . . . 8 (((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) ∧ π‘₯ β‰  βˆ…) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ ∩ π‘₯ β‰  βˆ…))
5216, 51pm2.61dane 3027 . . . . . . 7 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (π‘₯ βŠ† (Clsdβ€˜π½) ∧ Β¬ βˆ… ∈ (fiβ€˜π‘₯))) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ ∩ π‘₯ β‰  βˆ…))
5352expr 455 . . . . . 6 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ π‘₯ βŠ† (Clsdβ€˜π½)) β†’ (Β¬ βˆ… ∈ (fiβ€˜π‘₯) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ ∩ π‘₯ β‰  βˆ…)))
548, 53sylan2 591 . . . . 5 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ π‘₯ ∈ 𝒫 (Clsdβ€˜π½)) β†’ (Β¬ βˆ… ∈ (fiβ€˜π‘₯) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ ∩ π‘₯ β‰  βˆ…)))
5554com23 86 . . . 4 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ π‘₯ ∈ 𝒫 (Clsdβ€˜π½)) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ (Β¬ βˆ… ∈ (fiβ€˜π‘₯) β†’ ∩ π‘₯ β‰  βˆ…)))
5655ralrimdva 3152 . . 3 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ βˆ€π‘₯ ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘₯) β†’ ∩ π‘₯ β‰  βˆ…)))
57 topontop 22635 . . . 4 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
58 cmpfi 23132 . . . 4 (𝐽 ∈ Top β†’ (𝐽 ∈ Comp ↔ βˆ€π‘₯ ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘₯) β†’ ∩ π‘₯ β‰  βˆ…)))
5957, 58syl 17 . . 3 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (𝐽 ∈ Comp ↔ βˆ€π‘₯ ∈ 𝒫 (Clsdβ€˜π½)(Β¬ βˆ… ∈ (fiβ€˜π‘₯) β†’ ∩ π‘₯ β‰  βˆ…)))
6056, 59sylibrd 258 . 2 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ… β†’ 𝐽 ∈ Comp))
617, 60impbid 211 1 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ (𝐽 ∈ Comp ↔ βˆ€π‘“ ∈ (Filβ€˜π‘‹)(𝐽 fClus 𝑓) β‰  βˆ…))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  Vcvv 3472   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  βˆͺ cuni 4907  βˆ© cint 4949  β€˜cfv 6542  (class class class)co 7411  ficfi 9407  fBascfbas 21132  filGencfg 21133  Topctop 22615  TopOnctopon 22632  Clsdccld 22740  clsccl 22742  Compccmp 23110  Filcfil 23569   fClus cfcls 23660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1o 8468  df-er 8705  df-en 8942  df-fin 8945  df-fi 9408  df-fbas 21141  df-fg 21142  df-top 22616  df-topon 22633  df-cld 22743  df-cls 22745  df-cmp 23111  df-fil 23570  df-fcls 23665
This theorem is referenced by:  ufilcmp  23756
  Copyright terms: Public domain W3C validator