Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  flimfnfcls Unicode version

Theorem flimfnfcls 18013
 Description: A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 18012, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Hypothesis
Ref Expression
flimfnfcls.x
Assertion
Ref Expression
flimfnfcls
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem flimfnfcls
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 flimfcls 18011 . . . . 5
2 flimtop 17950 . . . . . . . . 9
3 flimfnfcls.x . . . . . . . . . 10
43toptopon 16953 . . . . . . . . 9 TopOn
52, 4sylib 189 . . . . . . . 8 TopOn
65ad2antrr 707 . . . . . . 7 TopOn
7 simplr 732 . . . . . . 7
8 simpr 448 . . . . . . 7
9 flimss2 17957 . . . . . . 7 TopOn
106, 7, 8, 9syl3anc 1184 . . . . . 6
11 simpll 731 . . . . . 6
1210, 11sseldd 3309 . . . . 5
131, 12sseldi 3306 . . . 4
1413ex 424 . . 3
1514ralrimiva 2749 . 2
16 sseq2 3330 . . . . . 6
17 oveq2 6048 . . . . . . 7
1817eleq2d 2471 . . . . . 6
1916, 18imbi12d 312 . . . . 5
2019rspcv 3008 . . . 4
21 ssid 3327 . . . . . 6
22 id 20 . . . . . 6
2321, 22mpi 17 . . . . 5
24 fclstop 17996 . . . . . 6
253fclselbas 18001 . . . . . 6
2624, 25jca 519 . . . . 5
2723, 26syl 16 . . . 4
2820, 27syl6 31 . . 3
29 disjdif 3660 . . . . . . . . . . . . . 14
30 simpll 731 . . . . . . . . . . . . . . . . . . . . 21
31 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . 23
323topopn 16934 . . . . . . . . . . . . . . . . . . . . . . 23
3331, 32syl 16 . . . . . . . . . . . . . . . . . . . . . 22
34 pwexg 4343 . . . . . . . . . . . . . . . . . . . . . 22
35 rabexg 4313 . . . . . . . . . . . . . . . . . . . . . 22
3633, 34, 353syl 19 . . . . . . . . . . . . . . . . . . . . 21
37 unexg 4669 . . . . . . . . . . . . . . . . . . . . 21
3830, 36, 37syl2anc 643 . . . . . . . . . . . . . . . . . . . 20
39 ssfii 7382 . . . . . . . . . . . . . . . . . . . 20
4038, 39syl 16 . . . . . . . . . . . . . . . . . . 19
41 filsspw 17836 . . . . . . . . . . . . . . . . . . . . . . 23
42 ssrab2 3388 . . . . . . . . . . . . . . . . . . . . . . . 24
4342a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
4441, 43unssd 3483 . . . . . . . . . . . . . . . . . . . . . 22
4544ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
46 ssun2 3471 . . . . . . . . . . . . . . . . . . . . . . 23
47 difss 3434 . . . . . . . . . . . . . . . . . . . . . . . . 25
48 elpw2g 4323 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4933, 48syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
5047, 49mpbiri 225 . . . . . . . . . . . . . . . . . . . . . . . 24
51 ssid 3327 . . . . . . . . . . . . . . . . . . . . . . . . 25
5251a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
53 sseq2 3330 . . . . . . . . . . . . . . . . . . . . . . . . 25
5453elrab 3052 . . . . . . . . . . . . . . . . . . . . . . . 24
5550, 52, 54sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . . 23
5646, 55sseldi 3306 . . . . . . . . . . . . . . . . . . . . . 22
57 ne0i 3594 . . . . . . . . . . . . . . . . . . . . . 22
5856, 57syl 16 . . . . . . . . . . . . . . . . . . . . 21
59 sseq2 3330 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
6059elrab 3052 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
6160simprbi 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6261ad2antll 710 . . . . . . . . . . . . . . . . . . . . . . . . 25
63 sslin 3527 . . . . . . . . . . . . . . . . . . . . . . . . 25
6462, 63syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24
65 simprrr 742 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6665adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25
67 inssdif0 3655 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
68 simplll 735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
70 filelss 17837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
7168, 69, 70syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
72 df-ss 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
7371, 72sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7473sseq1d 3335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7530ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
77 elssuni 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7877, 3syl6sseqr 3355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
7978ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8079ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
81 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
82 filss 17838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8375, 76, 80, 81, 82syl13anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8483ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
8574, 84sylbid 207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8667, 85syl5bir 210 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8786necon3bd 2604 . . . . . . . . . . . . . . . . . . . . . . . . 25
8866, 87mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24
89 ssn0 3620 . . . . . . . . . . . . . . . . . . . . . . . 24
9064, 88, 89syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23
9190ralrimivva 2758 . . . . . . . . . . . . . . . . . . . . . 22
92 filfbas 17833 . . . . . . . . . . . . . . . . . . . . . . . 24
9330, 92syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
9447a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25
95 filtop 17840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9630, 95syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
97 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9896, 97syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9998necon3bd 2604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10065, 99mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26
101 pssdifn0 3649 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10279, 100, 101syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
103 supfil 17880 . . . . . . . . . . . . . . . . . . . . . . . . 25
10433, 94, 102, 103syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . . 24
105 filfbas 17833 . . . . . . . . . . . . . . . . . . . . . . . 24
106104, 105syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
107 fbunfip 17854 . . . . . . . . . . . . . . . . . . . . . . 23
10893, 106, 107syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
10991, 108mpbird 224 . . . . . . . . . . . . . . . . . . . . 21
110 fsubbas 17852 . . . . . . . . . . . . . . . . . . . . . 22
11196, 110syl 16 . . . . . . . . . . . . . . . . . . . . 21
11245, 58, 109, 111mpbir3and 1137 . . . . . . . . . . . . . . . . . . . 20
113 ssfg 17857 . . . . . . . . . . . . . . . . . . . 20
114112, 113syl 16 . . . . . . . . . . . . . . . . . . 19
11540, 114sstrd 3318 . . . . . . . . . . . . . . . . . 18
116115unssad 3484 . . . . . . . . . . . . . . . . 17
117 fgcl 17863 . . . . . . . . . . . . . . . . . . 19
118112, 117syl 16 . . . . . . . . . . . . . . . . . 18
119 sseq2 3330 . . . . . . . . . . . . . . . . . . . 20
120 oveq2 6048 . . . . . . . . . . . . . . . . . . . . 21
121120eleq2d 2471 . . . . . . . . . . . . . . . . . . . 20
122119, 121imbi12d 312 . . . . . . . . . . . . . . . . . . 19
123122rspcv 3008 . . . . . . . . . . . . . . . . . 18
124118, 123syl 16 . . . . . . . . . . . . . . . . 17
125116, 124mpid 39 . . . . . . . . . . . . . . . 16
126 simpr 448 . . . . . . . . . . . . . . . . . 18
127 simplrl 737 . . . . . . . . . . . . . . . . . 18
128 simprrl 741 . . . . . . . . . . . . . . . . . . 19
129128adantr 452 . . . . . . . . . . . . . . . . . 18
130115, 56sseldd 3309 . . . . . . . . . . . . . . . . . . 19
131130adantr 452 . . . . . . . . . . . . . . . . . 18
132 fclsopni 18000 . . . . . . . . . . . . . . . . . 18
133126, 127, 129, 131, 132syl13anc 1186 . . . . . . . . . . . . . . . . 17
134133ex 424 . . . . . . . . . . . . . . . 16
135125, 134syld 42 . . . . . . . . . . . . . . 15
136135necon2bd 2616 . . . . . . . . . . . . . 14
13729, 136mpi 17 . . . . . . . . . . . . 13
138137anassrs 630 . . . . . . . . . . . 12
139138expr 599 . . . . . . . . . . 11
140139con4d 99 . . . . . . . . . 10
141140ex 424 . . . . . . . . 9
142141com23 74 . . . . . . . 8
143142ralrimdva 2756 . . . . . . 7
144 simprr 734 . . . . . . 7
145143, 144jctild 528 . . . . . 6
146 simprl 733 . . . . . . . 8
147146, 4sylib 189 . . . . . . 7 TopOn
148 simpl 444 . . . . . . 7
149 flimopn 17960 . . . . . . 7 TopOn
150147, 148, 149syl2anc 643 . . . . . 6
151145, 150sylibrd 226 . . . . 5
152151ex 424 . . . 4
153152com23 74 . . 3
15428, 153mpdd 38 . 2
15515, 154impbid2 196 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2567  wral 2666  crab 2670  cvv 2916   cdif 3277   cun 3278   cin 3279   wss 3280  c0 3588  cpw 3759  cuni 3975  cfv 5413  (class class class)co 6040  cfi 7373  cfbas 16644  cfg 16645  ctop 16913  TopOnctopon 16914  cfil 17830   cflim 17919   cfcls 17921 This theorem is referenced by:  cnpfcf  18026 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-en 7069  df-fin 7072  df-fi 7374  df-fbas 16654  df-fg 16655  df-top 16918  df-topon 16921  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-fil 17831  df-flim 17924  df-fcls 17926
 Copyright terms: Public domain W3C validator