Metamath Proof Explorer

Theorem isfcls

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

Ref Expression
Hypothesis fclsval.x 
|- X = U. J
Assertion isfcls 
|- ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )

Proof

Step Hyp Ref Expression
1 fclsval.x 
 |-  X = U. J
2 anass 
 |-  ( ( ( ( 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 ) ) ) )
3 fvssunirn 
 |-  ( Fil ` X ) C_ U. ran Fil
4 3 sseli 
 |-  ( F e. ( Fil ` X ) -> F e. U. ran Fil )
5 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
6 5 eqcomd 
 |-  ( F e. ( Fil ` X ) -> X = U. F )
7 4 6 jca 
 |-  ( F e. ( Fil ` X ) -> ( F e. U. ran Fil /\ X = U. F ) )
8 filunirn 
 |-  ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )
9 fveq2 
 |-  ( X = U. F -> ( Fil ` X ) = ( Fil ` U. F ) )
10 9 eleq2d 
 |-  ( X = U. F -> ( F e. ( Fil ` X ) <-> F e. ( Fil ` U. F ) ) )
11 10 biimparc 
 |-  ( ( F e. ( Fil ` U. F ) /\ X = U. F ) -> F e. ( Fil ` X ) )
12 8 11 sylanb 
 |-  ( ( F e. U. ran Fil /\ X = U. F ) -> F e. ( Fil ` X ) )
13 7 12 impbii 
 |-  ( F e. ( Fil ` X ) <-> ( F e. U. ran Fil /\ X = U. F ) )
14 13 anbi2i 
 |-  ( ( J e. Top /\ F e. ( Fil ` X ) ) <-> ( J e. Top /\ ( F e. U. ran Fil /\ X = U. F ) ) )
15 14 anbi1i 
 |-  ( ( ( 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 ) ) )
16 df-3an 
 |-  ( ( 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 ) ) )
17 anass 
 |-  ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) <-> ( J e. Top /\ ( F e. U. ran Fil /\ X = U. F ) ) )
18 17 anbi1i 
 |-  ( ( ( ( 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 ) ) )
19 15 16 18 3bitr4i 
 |-  ( ( 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 ) ) )
20 df-fcls 
 |-  fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ x e. f ( ( cls ` j ) ` x ) , (/) ) )
21 20 elmpocl 
 |-  ( A e. ( J fClus F ) -> ( J e. Top /\ F e. U. ran Fil ) )
22 1 fclsval 
 |-  ( ( J e. Top /\ F e. ( Fil ` U. F ) ) -> ( J fClus F ) = if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) )
23 8 22 sylan2b 
 |-  ( ( J e. Top /\ F e. U. ran Fil ) -> ( J fClus F ) = if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) )
24 23 eleq2d 
 |-  ( ( 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 
 |-  ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) -> -. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = (/) )
26 iffalse 
 |-  ( -. X = U. F -> if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = (/) )
27 25 26 nsyl2 
 |-  ( A e. if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) -> X = U. F )
28 27 a1i 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( X = U. F -> if ( X = U. F , |^|_ s e. F ( ( cls ` J ) ` s ) , (/) ) = |^|_ s e. F ( ( cls ` J ) ` s ) )
31 30 adantl 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) -> A e. _V )
34 33 a1i 
 |-  ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) -> A e. _V ) )
35 filn0 
 |-  ( F e. ( Fil ` U. F ) -> F =/= (/) )
36 8 35 sylbi 
 |-  ( F e. U. ran Fil -> F =/= (/) )
37 36 ad2antlr 
 |-  ( ( ( J e. Top /\ F e. U. ran Fil ) /\ X = U. F ) -> F =/= (/) )
38 r19.2z 
 |-  ( ( F =/= (/) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) -> E. s e. F A e. ( ( cls ` J ) ` s ) )
39 38 ex 
 |-  ( F =/= (/) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> E. s e. F A e. ( ( cls ` J ) ` s ) ) )
40 37 39 syl 
 |-  ( ( ( 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 
 |-  ( A e. ( ( cls ` J ) ` s ) -> A e. _V )
42 41 rexlimivw 
 |-  ( E. s e. F A e. ( ( cls ` J ) ` s ) -> A e. _V )
43 40 42 syl6 
 |-  ( ( ( 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 
 |-  ( A e. _V -> ( A e. |^|_ s e. F ( ( cls ` J ) ` s ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
45 44 a1i 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 
 |-  ( ( 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 21 49 biadanii 
 |-  ( 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 2 19 50 3bitr4ri 
 |-  ( A e. ( J fClus F ) <-> ( J e. Top /\ F e. ( Fil ` X ) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) )