Metamath Proof Explorer

Theorem fclsval

Description: The set of all cluster points 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 fclsval 
|- ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> ( J fClus F ) = if ( X = Y , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )

Proof

Step Hyp Ref Expression
1 fclsval.x 
 |-  X = U. J
2 simpl 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> J e. Top )
3 fvssunirn 
 |-  ( Fil ` Y ) C_ U. ran Fil
4 3 sseli 
 |-  ( F e. ( Fil ` Y ) -> F e. U. ran Fil )
5 4 adantl 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> F e. U. ran Fil )
6 filn0 
 |-  ( F e. ( Fil ` Y ) -> F =/= (/) )
7 6 adantl 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> F =/= (/) )
8 fvex 
 |-  ( ( cls ` J ) ` t ) e. _V
9 8 rgenw 
 |-  A. t e. F ( ( cls ` J ) ` t ) e. _V
10 iinexg 
 |-  ( ( F =/= (/) /\ A. t e. F ( ( cls ` J ) ` t ) e. _V ) -> |^|_ t e. F ( ( cls ` J ) ` t ) e. _V )
11 7 9 10 sylancl 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> |^|_ t e. F ( ( cls ` J ) ` t ) e. _V )
12 0ex 
 |-  (/) e. _V
13 ifcl 
 |-  ( ( |^|_ t e. F ( ( cls ` J ) ` t ) e. _V /\ (/) e. _V ) -> if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) e. _V )
14 11 12 13 sylancl 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) e. _V )
15 unieq 
 |-  ( j = J -> U. j = U. J )
16 15 1 eqtr4di 
 |-  ( j = J -> U. j = X )
17 unieq 
 |-  ( f = F -> U. f = U. F )
18 16 17 eqeqan12d 
 |-  ( ( j = J /\ f = F ) -> ( U. j = U. f <-> X = U. F ) )
19 iineq1 
 |-  ( f = F -> |^|_ t e. f ( ( cls ` j ) ` t ) = |^|_ t e. F ( ( cls ` j ) ` t ) )
20 19 adantl 
 |-  ( ( j = J /\ f = F ) -> |^|_ t e. f ( ( cls ` j ) ` t ) = |^|_ t e. F ( ( cls ` j ) ` t ) )
21 simpll 
 |-  ( ( ( j = J /\ f = F ) /\ t e. F ) -> j = J )
22 21 fveq2d 
 |-  ( ( ( j = J /\ f = F ) /\ t e. F ) -> ( cls ` j ) = ( cls ` J ) )
23 22 fveq1d 
 |-  ( ( ( j = J /\ f = F ) /\ t e. F ) -> ( ( cls ` j ) ` t ) = ( ( cls ` J ) ` t ) )
24 23 iineq2dv 
 |-  ( ( j = J /\ f = F ) -> |^|_ t e. F ( ( cls ` j ) ` t ) = |^|_ t e. F ( ( cls ` J ) ` t ) )
25 20 24 eqtrd 
 |-  ( ( j = J /\ f = F ) -> |^|_ t e. f ( ( cls ` j ) ` t ) = |^|_ t e. F ( ( cls ` J ) ` t ) )
26 18 25 ifbieq1d 
 |-  ( ( j = J /\ f = F ) -> if ( U. j = U. f , |^|_ t e. f ( ( cls ` j ) ` t ) , (/) ) = if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )
27 df-fcls 
 |-  fClus = ( j e. Top , f e. U. ran Fil |-> if ( U. j = U. f , |^|_ t e. f ( ( cls ` j ) ` t ) , (/) ) )
28 26 27 ovmpoga 
 |-  ( ( J e. Top /\ F e. U. ran Fil /\ if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) e. _V ) -> ( J fClus F ) = if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )
29 2 5 14 28 syl3anc 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> ( J fClus F ) = if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )
30 filunibas 
 |-  ( F e. ( Fil ` Y ) -> U. F = Y )
31 30 eqeq2d 
 |-  ( F e. ( Fil ` Y ) -> ( X = U. F <-> X = Y ) )
32 31 adantl 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> ( X = U. F <-> X = Y ) )
33 32 ifbid 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> if ( X = U. F , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) = if ( X = Y , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )
34 29 33 eqtrd 
 |-  ( ( J e. Top /\ F e. ( Fil ` Y ) ) -> ( J fClus F ) = if ( X = Y , |^|_ t e. F ( ( cls ` J ) ` t ) , (/) ) )