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 ) ) )