Theorem isfcls 17994

Description: A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)

Hypothesis

Ref	Expression
fclsval.x	|- X = U. J

Assertion

Ref	Expression
isfcls	|- ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )

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

Proof of Theorem isfcls

Dummy variables f j x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		anass 631	. 2 |- ( ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( ( J e. Top /\ F e. U. ran Fil ) /\ ( X = U. F /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) ) )
2		fvssunirn 5713	. . . . . . . 8 |- ( Fil ` X ) C_ U. ran Fil
3	2	sseli 3304	. . . . . . 7 |- ( F e. ( Fil ` X ) -> F e. U. ran Fil )
4		filunibas 17866	. . . . . . . 8 |- ( F e. ( Fil ` X ) -> U. F = X )
5	4	eqcomd 2409	. . . . . . 7 |- ( F e. ( Fil ` X ) -> X = U. F )
6	3, 5	jca 519	. . . . . 6 |- ( F e. ( Fil ` X ) -> ( F e. U. ran Fil /\ X = U. F ) )
7		filunirn 17867	. . . . . . 7 |- ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )
8		fveq2 5687	. . . . . . . . 9 |- ( X = U. F -> ( Fil ` X ) = ( Fil ` U. F ) )
9	8	eleq2d 2471	. . . . . . . 8 |- ( X = U. F -> ( F e. ( Fil ` X ) <-> F e. ( Fil ` U. F ) ) )
10	9	biimparc 474	. . . . . . 7 |- ( ( F e. ( Fil ` U. F ) /\ X = U. F ) -> F e. ( Fil ` X ) )
11	7, 10	sylanb 459	. . . . . 6 |- ( ( F e. U. ran Fil /\ X = U. F ) -> F e. ( Fil ` X ) )
12	6, 11	impbii 181	. . . . 5 |- ( F e. ( Fil ` X ) <-> ( F e. U. ran Fil /\ X = U. F ) )
13	12	anbi2i 676	. . . 4 |- ( ( J e. Top /\ F e. ( Fil ` X ) ) <-> ( J e. Top /\ ( F e. U. ran Fil /\ X = U. F ) ) )
14	13	anbi1i 677	. . 3 |- ( ( ( J e. Top /\ F e. ( Fil ` X ) ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( ( J e. Top /\ ( F e. U. ran Fil /\ X = U. F ) ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
15		df-3an 938	. . 3 |- ( ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( ( J e. Top /\ F e. ( Fil ` X ) ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
16		anass 631	. . . 4 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) <-> ( J e. Top /\ ( F e. U. ran Fil /\ X = U. F ) ) )
17	16	anbi1i 677	. . 3 |- ( ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( ( J e. Top /\ ( F e. U. ran Fil /\ X = U. F ) ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
18	14, 15, 17	3bitr4i 269	. 2 |- ( ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )
19		df-fcls 17926	. . . 4 |- fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )
20	19	elmpt2cl 6247	. . 3 |- ( A e. ( J fClus F ) -> ( J e. Top /\ F e. U. ran Fil ) )
21		fclsval.x	. . . . . . 7 |- X = U. J
22	21	fclsval 17993	. . . . . 6 |- ( ( J e. Top /\ F e. ( Fil ` U. F ) ) -> ( J fClus F ) = if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) )
23	7, 22	sylan2b 462	. . . . 5 |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fClus F ) = if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) )
24	23	eleq2d 2471	. . . 4 |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( A e. ( J fClus F ) <-> A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) ) )
25		n0i 3593	. . . . . . 7 |- ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) -> -. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = (/) )
26		iffalse 3706	. . . . . . 7 |- ( -. X = U. F -> if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = (/) )
27	25, 26	nsyl2 121	. . . . . 6 |- ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) -> X = U. F )
28	27	a1i 11	. . . . 5 |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) -> X = U. F ) )
29	28	pm4.71rd 617	. . . 4 |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) <-> ( X = U. F /\ A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) ) ) )
30		iftrue 3705	. . . . . . . 8 |- ( X = U. F -> if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = |^|_ s e. F ( ( cls ` J ) ` s ) )
31	30	adantl 453	. . . . . . 7 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = |^|_ s e. F ( ( cls ` J ) ` s ) )
32	31	eleq2d 2471	. . . . . 6 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) <-> A e. |^|_ s e. F ( ( cls ` J ) ` s ) ) )
33		elex 2924	. . . . . . . 8 |- ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) -> A e. _V )
34	33	a1i 11	. . . . . . 7 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) -> A e. _V ) )
35		filn0 17847	. . . . . . . . . . 11 |- ( F e. ( Fil ` U. F ) -> F =/= (/) )
36	7, 35	sylbi 188	. . . . . . . . . 10 |- ( F e. U. ran Fil -> F =/= (/) )
37	36	ad2antlr 708	. . . . . . . . 9 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> F =/= (/) )
38		r19.2z 3677	. . . . . . . . . 10 |- ( ( F =/= (/) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) -> E. s e. F A e. ( ( cls ` J ) ` s ) )
39	38	ex 424	. . . . . . . . 9 |- ( F =/= (/) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> E. s e. F A e. ( ( cls ` J ) ` s ) ) )
40	37, 39	syl 16	. . . . . . . 8 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> E. s e. F A e. ( ( cls ` J ) ` s ) ) )
41		elex 2924	. . . . . . . . 9 |- ( A e. ( ( cls ` J ) ` s ) -> A e. _V )
42	41	rexlimivw 2786	. . . . . . . 8 |- ( E. s e. F A e. ( ( cls ` J ) ` s ) -> A e. _V )
43	40, 42	syl6 31	. . . . . . 7 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> A e. _V ) )
44		eliin 4058	. . . . . . . 8 |- ( A e. _V -> ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
45	44	a1i 11	. . . . . . 7 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A e. _V -> ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) ) )
46	34, 43, 45	pm5.21ndd 344	. . . . . 6 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
47	32, 46	bitrd 245	. . . . 5 |- ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
48	47	pm5.32da 623	. . . 4 |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( ( X = U. F /\ A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) ) <-> ( X = U. F /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) ) )
49	24, 29, 48	3bitrd 271	. . 3 |- ( ( J e. Top /\ F e. U. ran Fil ) -> ( A e. ( J fClus F ) <-> ( X = U. F /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) ) )
50	20, 49	biadan2 624	. 2 |- ( A e. ( J fClus F ) <-> ( ( J e. Top /\ F e. U. ran Fil ) /\ ( X = U. F /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) ) )
51	1, 18, 50	3bitr4ri 270	1 |- ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   _Vcvv 2916   (/)c0 3588   ifcif 3699   U.cuni 3975   |^|_ciin 4054   ran crn 4838   ` cfv 5413  (class class class)co 6040   Topctop 16913   clsccl 17037   Filcfil 17830   fClus cfcls 17921

This theorem is referenced by:  fclsfil  17995  fclstop  17996  isfcls2  17998  fclssscls  18003  flimfcls  18011

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-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  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-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  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-id 4458  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-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-fbas 16654  df-fil 17831  df-fcls 17926