Metamath Proof Explorer

Theorem fcfval

Description: The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfval 
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )

Proof

Step Hyp Ref Expression
1 df-fcf 
 |-  fClusf = ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) )
2 1 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> fClusf = ( j e. Top , f e. U. ran Fil |-> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) ) )
3 simprl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> j = J )
4 3 unieqd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> U. j = U. J )
5 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
6 5 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> X = U. J )
7 4 6 eqtr4d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> U. j = X )
8 unieq 
 |-  ( f = L -> U. f = U. L )
9 8 ad2antll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> U. f = U. L )
10 filunibas 
 |-  ( L e. ( Fil ` Y ) -> U. L = Y )
11 10 ad2antlr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> U. L = Y )
12 9 11 eqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> U. f = Y )
13 7 12 oveq12d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> ( U. j ^m U. f ) = ( X ^m Y ) )
14 7 oveq1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> ( U. j FilMap g ) = ( X FilMap g ) )
15 simprr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> f = L )
16 14 15 fveq12d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> ( ( U. j FilMap g ) ` f ) = ( ( X FilMap g ) ` L ) )
17 3 16 oveq12d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> ( j fClus ( ( U. j FilMap g ) ` f ) ) = ( J fClus ( ( X FilMap g ) ` L ) ) )
18 13 17 mpteq12dv 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) /\ ( j = J /\ f = L ) ) -> ( g e. ( U. j ^m U. f ) |-> ( j fClus ( ( U. j FilMap g ) ` f ) ) ) = ( g e. ( X ^m Y ) |-> ( J fClus ( ( X FilMap g ) ` L ) ) ) )
19 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
20 19 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> J e. Top )
21 fvssunirn 
 |-  ( Fil ` Y ) C_ U. ran Fil
22 21 sseli 
 |-  ( L e. ( Fil ` Y ) -> L e. U. ran Fil )
23 22 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> L e. U. ran Fil )
24 ovex 
 |-  ( X ^m Y ) e. _V
25 24 mptex 
 |-  ( g e. ( X ^m Y ) |-> ( J fClus ( ( X FilMap g ) ` L ) ) ) e. _V
26 25 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( g e. ( X ^m Y ) |-> ( J fClus ( ( X FilMap g ) ` L ) ) ) e. _V )
27 2 18 20 23 26 ovmpod 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fClusf L ) = ( g e. ( X ^m Y ) |-> ( J fClus ( ( X FilMap g ) ` L ) ) ) )
28 27 3adant3 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( J fClusf L ) = ( g e. ( X ^m Y ) |-> ( J fClus ( ( X FilMap g ) ` L ) ) ) )
29 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ g = F ) -> g = F )
30 29 oveq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ g = F ) -> ( X FilMap g ) = ( X FilMap F ) )
31 30 fveq1d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ g = F ) -> ( ( X FilMap g ) ` L ) = ( ( X FilMap F ) ` L ) )
32 31 oveq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ g = F ) -> ( J fClus ( ( X FilMap g ) ` L ) ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
33 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
34 filtop 
 |-  ( L e. ( Fil ` Y ) -> Y e. L )
35 elmapg 
 |-  ( ( X e. J /\ Y e. L ) -> ( F e. ( X ^m Y ) <-> F : Y --> X ) )
36 33 34 35 syl2an 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( F e. ( X ^m Y ) <-> F : Y --> X ) )
37 36 biimp3ar 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> F e. ( X ^m Y ) )
38 ovexd 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( J fClus ( ( X FilMap F ) ` L ) ) e. _V )
39 28 32 37 38 fvmptd 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )