Theorem fclsfnflim 20820

Description: A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)

Assertion

Ref	Expression
fclsfnflim	|- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) <-> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )

Distinct variable groups:   A, g   g, F   g, J   g, X

Proof of Theorem fclsfnflim

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		filsspw 20644	. . . . . . . 8 |- ( F e. ( Fil ` X ) -> F C_ ~P X )
2	1	adantr 463	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ~P X )
3		fclstop 20804	. . . . . . . . . 10 |- ( A e. ( J fClus F ) -> J e. Top )
4	3	adantl 464	. . . . . . . . 9 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> J e. Top )
5		eqid 2402	. . . . . . . . . 10 |- U. J = U. J
6	5	neisspw 19901	. . . . . . . . 9 |- ( J e. Top -> ( ( nei ` J ) ` { A } ) C_ ~P U. J )
7	4, 6	syl 17	. . . . . . . 8 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P U. J )
8		filunibas 20674	. . . . . . . . . 10 |- ( F e. ( Fil ` X ) -> U. F = X )
9	5	fclsfil 20803	. . . . . . . . . . 11 |- ( A e. ( J fClus F ) -> F e. ( Fil ` U. J ) )
10		filunibas 20674	. . . . . . . . . . 11 |- ( F e. ( Fil ` U. J ) -> U. F = U. J )
11	9, 10	syl 17	. . . . . . . . . 10 |- ( A e. ( J fClus F ) -> U. F = U. J )
12	8, 11	sylan9req 2464	. . . . . . . . 9 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> X = U. J )
13	12	pweqd 3960	. . . . . . . 8 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ~P X = ~P U. J )
14	7, 13	sseqtr4d 3479	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ~P X )
15	2, 14	unssd 3619	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X )
16		ssun1 3606	. . . . . . . 8 |- F C_ ( F u. ( ( nei ` J ) ` { A } ) )
17		filn0 20655	. . . . . . . 8 |- ( F e. ( Fil ` X ) -> F =/= (/) )
18		ssn0 3772	. . . . . . . 8 |- ( ( F C_ ( F u. ( ( nei ` J ) ` { A } ) ) /\ F =/= (/) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) )
19	16, 17, 18	sylancr 661	. . . . . . 7 |- ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) )
20	19	adantr 463	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) )
21		incom 3632	. . . . . . . . . . . 12 |- ( y i^i x ) = ( x i^i y )
22		fclsneii 20810	. . . . . . . . . . . 12 |- ( ( A e. ( J fClus F ) /\ y e. ( ( nei ` J ) ` { A } ) /\ x e. F ) -> ( y i^i x ) =/= (/) )
23	21, 22	syl5eqner 2704	. . . . . . . . . . 11 |- ( ( A e. ( J fClus F ) /\ y e. ( ( nei ` J ) ` { A } ) /\ x e. F ) -> ( x i^i y ) =/= (/) )
24	23	3com23 1203	. . . . . . . . . 10 |- ( ( A e. ( J fClus F ) /\ x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( x i^i y ) =/= (/) )
25	24	3expb 1198	. . . . . . . . 9 |- ( ( A e. ( J fClus F ) /\ ( x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i y ) =/= (/) )
26	25	adantll 712	. . . . . . . 8 |- ( ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) /\ ( x e. F /\ y e. ( ( nei ` J ) ` { A } ) ) ) -> ( x i^i y ) =/= (/) )
27	26	ralrimivva 2825	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) )
28		filfbas 20641	. . . . . . . . 9 |- ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
29	28	adantr 463	. . . . . . . 8 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F e. ( fBas ` X ) )
30		istopon 19718	. . . . . . . . . . 11 |- ( J e. (TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
31	4, 12, 30	sylanbrc 662	. . . . . . . . . 10 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> J e. (TopOn ` X ) )
32	5	fclselbas 20809	. . . . . . . . . . . . 13 |- ( A e. ( J fClus F ) -> A e. U. J )
33	32	adantl 464	. . . . . . . . . . . 12 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. U. J )
34	33, 12	eleqtrrd 2493	. . . . . . . . . . 11 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. X )
35	34	snssd 4117	. . . . . . . . . 10 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> { A } C_ X )
36		snnzg 4089	. . . . . . . . . . 11 |- ( A e. ( J fClus F ) -> { A } =/= (/) )
37	36	adantl 464	. . . . . . . . . 10 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> { A } =/= (/) )
38		neifil 20673	. . . . . . . . . 10 |- ( ( J e. (TopOn ` X ) /\ { A } C_ X /\ { A } =/= (/) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
39	31, 35, 37, 38	syl3anc 1230	. . . . . . . . 9 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) )
40		filfbas 20641	. . . . . . . . 9 |- ( ( ( nei ` J ) ` { A } ) e. ( Fil ` X ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) )
41	39, 40	syl 17	. . . . . . . 8 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) )
42		fbunfip 20662	. . . . . . . 8 |- ( ( F e. ( fBas ` X ) /\ ( ( nei ` J ) ` { A } ) e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) <-> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) )
43	29, 41, 42	syl2anc 659	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) <-> A. x e. F A. y e. ( ( nei ` J ) ` { A } ) ( x i^i y ) =/= (/) ) )
44	27, 43	mpbird 232	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
45		filtop 20648	. . . . . . . 8 |- ( F e. ( Fil ` X ) -> X e. F )
46		fsubbas 20660	. . . . . . . 8 |- ( X e. F -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
47	45, 46	syl 17	. . . . . . 7 |- ( F e. ( Fil ` X ) -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
48	47	adantr 463	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) <-> ( ( F u. ( ( nei ` J ) ` { A } ) ) C_ ~P X /\ ( F u. ( ( nei ` J ) ` { A } ) ) =/= (/) /\ -. (/) e. ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
49	15, 20, 44, 48	mpbir3and 1180	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) )
50		fgcl 20671	. . . . 5 |- ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) )
51	49, 50	syl 17	. . . 4 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) )
52		fvex 5859	. . . . . . . . 9 |- ( ( nei ` J ) ` { A } ) e. _V
53		unexg 6583	. . . . . . . . 9 |- ( ( F e. ( Fil ` X ) /\ ( ( nei ` J ) ` { A } ) e. _V ) -> ( F u. ( ( nei ` J ) ` { A } ) ) e. _V )
54	52, 53	mpan2 669	. . . . . . . 8 |- ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) e. _V )
55		ssfii 7913	. . . . . . . 8 |- ( ( F u. ( ( nei ` J ) ` { A } ) ) e. _V -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
56	54, 55	syl 17	. . . . . . 7 |- ( F e. ( Fil ` X ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
57	56	adantr 463	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( F u. ( ( nei ` J ) ` { A } ) ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
58	57	unssad 3620	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
59		ssfg 20665	. . . . . 6 |- ( ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) e. ( fBas ` X ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
60	49, 59	syl 17	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
61	58, 60	sstrd 3452	. . . 4 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
62	57	unssbd 3621	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) )
63	62, 60	sstrd 3452	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) )
64		elflim 20764	. . . . . 6 |- ( ( J e. (TopOn ` X ) /\ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) ) -> ( A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) )
65	31, 51, 64	syl2anc 659	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> ( A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) )
66	34, 63, 65	mpbir2and 923	. . . 4 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
67		sseq2 3464	. . . . . 6 |- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( F C_ g <-> F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
68		oveq2 6286	. . . . . . 7 |- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( J fLim g ) = ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) )
69	68	eleq2d 2472	. . . . . 6 |- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( A e. ( J fLim g ) <-> A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) )
70	67, 69	anbi12d 709	. . . . 5 |- ( g = ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) -> ( ( F C_ g /\ A e. ( J fLim g ) ) <-> ( F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) )
71	70	rspcev 3160	. . . 4 |- ( ( ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) e. ( Fil ` X ) /\ ( F C_ ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) /\ A e. ( J fLim ( X filGen ( fi ` ( F u. ( ( nei ` J ) ` { A } ) ) ) ) ) ) ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) )
72	51, 61, 66, 71	syl12anc 1228	. . 3 |- ( ( F e. ( Fil ` X ) /\ A e. ( J fClus F ) ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) )
73	72	ex 432	. 2 |- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) -> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )
74		simprl 756	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> g e. ( Fil ` X ) )
75		simprrr 767	. . . . . . 7 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fLim g ) )
76		flimtopon 20763	. . . . . . 7 |- ( A e. ( J fLim g ) -> ( J e. (TopOn ` X ) <-> g e. ( Fil ` X ) ) )
77	75, 76	syl 17	. . . . . 6 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> ( J e. (TopOn ` X ) <-> g e. ( Fil ` X ) ) )
78	74, 77	mpbird 232	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> J e. (TopOn ` X ) )
79		simpl 455	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> F e. ( Fil ` X ) )
80		simprrl 766	. . . . 5 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> F C_ g )
81		fclsss2 20816	. . . . 5 |- ( ( J e. (TopOn ` X ) /\ F e. ( Fil ` X ) /\ F C_ g ) -> ( J fClus g ) C_ ( J fClus F ) )
82	78, 79, 80, 81	syl3anc 1230	. . . 4 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> ( J fClus g ) C_ ( J fClus F ) )
83		flimfcls 20819	. . . . 5 |- ( J fLim g ) C_ ( J fClus g )
84	83, 75	sseldi 3440	. . . 4 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fClus g ) )
85	82, 84	sseldd 3443	. . 3 |- ( ( F e. ( Fil ` X ) /\ ( g e. ( Fil ` X ) /\ ( F C_ g /\ A e. ( J fLim g ) ) ) ) -> A e. ( J fClus F ) )
86	85	rexlimdvaa 2897	. 2 |- ( F e. ( Fil ` X ) -> ( E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) -> A e. ( J fClus F ) ) )
87	73, 86	impbid 190	1 |- ( F e. ( Fil ` X ) -> ( A e. ( J fClus F ) <-> E. g e. ( Fil ` X ) ( F C_ g /\ A e. ( J fLim g ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   =/= wne 2598   A.wral 2754   E.wrex 2755   _Vcvv 3059   u. cun 3412   i^i cin 3413   C_ wss 3414   (/)c0 3738   ~Pcpw 3955   {csn 3972   U.cuni 4191   ` cfv 5569  (class class class)co 6278   ficfi 7904   fBascfbas 18726   filGencfg 18727   Topctop 19686  TopOnctopon 19687   neicnei 19891   Filcfil 20638   fLim cflim 20727   fClus cfcls 20729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-int 4228  df-iun 4273  df-iin 4274  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-1o 7167  df-oadd 7171  df-er 7348  df-en 7555  df-fin 7558  df-fi 7905  df-fbas 18736  df-fg 18737  df-top 19691  df-topon 19694  df-cld 19812  df-ntr 19813  df-cls 19814  df-nei 19892  df-fil 20639  df-flim 20732  df-fcls 20734

This theorem is referenced by:  uffclsflim  20824  cnpfcfi  20833