Metamath Proof Explorer

Theorem flffval

Description: Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009) (Revised by Mario Carneiro, 15-Dec-2013) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flffval 
|- ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLimf L ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) )

Proof

Step Hyp Ref Expression
1 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
2 fvssunirn 
 |-  ( Fil ` Y ) C_ U. ran Fil
3 2 sseli 
 |-  ( L e. ( Fil ` Y ) -> L e. U. ran Fil )
4 unieq 
 |-  ( x = J -> U. x = U. J )
5 unieq 
 |-  ( y = L -> U. y = U. L )
6 4 5 oveqan12d 
 |-  ( ( x = J /\ y = L ) -> ( U. x ^m U. y ) = ( U. J ^m U. L ) )
7 simpl 
 |-  ( ( x = J /\ y = L ) -> x = J )
8 4 adantr 
 |-  ( ( x = J /\ y = L ) -> U. x = U. J )
9 8 oveq1d 
 |-  ( ( x = J /\ y = L ) -> ( U. x FilMap f ) = ( U. J FilMap f ) )
10 simpr 
 |-  ( ( x = J /\ y = L ) -> y = L )
11 9 10 fveq12d 
 |-  ( ( x = J /\ y = L ) -> ( ( U. x FilMap f ) ` y ) = ( ( U. J FilMap f ) ` L ) )
12 7 11 oveq12d 
 |-  ( ( x = J /\ y = L ) -> ( x fLim ( ( U. x FilMap f ) ` y ) ) = ( J fLim ( ( U. J FilMap f ) ` L ) ) )
13 6 12 mpteq12dv 
 |-  ( ( x = J /\ y = L ) -> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) = ( f e. ( U. J ^m U. L ) |-> ( J fLim ( ( U. J FilMap f ) ` L ) ) ) )
14 df-flf 
 |-  fLimf = ( x e. Top , y e. U. ran Fil |-> ( f e. ( U. x ^m U. y ) |-> ( x fLim ( ( U. x FilMap f ) ` y ) ) ) )
15 ovex 
 |-  ( U. J ^m U. L ) e. _V
16 15 mptex 
 |-  ( f e. ( U. J ^m U. L ) |-> ( J fLim ( ( U. J FilMap f ) ` L ) ) ) e. _V
17 13 14 16 ovmpoa 
 |-  ( ( J e. Top /\ L e. U. ran Fil ) -> ( J fLimf L ) = ( f e. ( U. J ^m U. L ) |-> ( J fLim ( ( U. J FilMap f ) ` L ) ) ) )
18 1 3 17 syl2an 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLimf L ) = ( f e. ( U. J ^m U. L ) |-> ( J fLim ( ( U. J FilMap f ) ` L ) ) ) )
19 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
20 19 eqcomd 
 |-  ( J e. ( TopOn ` X ) -> U. J = X )
21 filunibas 
 |-  ( L e. ( Fil ` Y ) -> U. L = Y )
22 20 21 oveqan12d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( U. J ^m U. L ) = ( X ^m Y ) )
23 20 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> U. J = X )
24 23 oveq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( U. J FilMap f ) = ( X FilMap f ) )
25 24 fveq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( ( U. J FilMap f ) ` L ) = ( ( X FilMap f ) ` L ) )
26 25 oveq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLim ( ( U. J FilMap f ) ` L ) ) = ( J fLim ( ( X FilMap f ) ` L ) ) )
27 22 26 mpteq12dv 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( f e. ( U. J ^m U. L ) |-> ( J fLim ( ( U. J FilMap f ) ` L ) ) ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) )
28 18 27 eqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) ) -> ( J fLimf L ) = ( f e. ( X ^m Y ) |-> ( J fLim ( ( X FilMap f ) ` L ) ) ) )