Metamath Proof Explorer

Theorem hlimf

Description: Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hlimf 
|- ~~>v : dom ~~>v --> ~H

Proof

Step Hyp Ref Expression
1 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
2 eqid 
 |-  ( IndMet ` <. <. +h , .h >. , normh >. ) = ( IndMet ` <. <. +h , .h >. , normh >. )
3 1 2 hhxmet 
 |-  ( IndMet ` <. <. +h , .h >. , normh >. ) e. ( *Met ` ~H )
4 eqid 
 |-  ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) = ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) )
5 4 methaus 
 |-  ( ( IndMet ` <. <. +h , .h >. , normh >. ) e. ( *Met ` ~H ) -> ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) e. Haus )
6 lmfun 
 |-  ( ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) e. Haus -> Fun ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) )
7 3 5 6 mp2b 
 |-  Fun ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) )
8 funres 
 |-  ( Fun ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) -> Fun ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) )
9 7 8 ax-mp 
 |-  Fun ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) )
10 1 2 4 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) )
11 10 funeqi 
 |-  ( Fun ~~>v <-> Fun ( ( ~~>t ` ( MetOpen ` ( IndMet ` <. <. +h , .h >. , normh >. ) ) ) |` ( ~H ^m NN ) ) )
12 9 11 mpbir 
 |-  Fun ~~>v
13 funfn 
 |-  ( Fun ~~>v <-> ~~>v Fn dom ~~>v )
14 12 13 mpbi 
 |-  ~~>v Fn dom ~~>v
15 funfvbrb 
 |-  ( Fun ~~>v -> ( x e. dom ~~>v <-> x ~~>v ( ~~>v ` x ) ) )
16 12 15 ax-mp 
 |-  ( x e. dom ~~>v <-> x ~~>v ( ~~>v ` x ) )
17 fvex 
 |-  ( ~~>v ` x ) e. _V
18 17 hlimveci 
 |-  ( x ~~>v ( ~~>v ` x ) -> ( ~~>v ` x ) e. ~H )
19 16 18 sylbi 
 |-  ( x e. dom ~~>v -> ( ~~>v ` x ) e. ~H )
20 19 rgen 
 |-  A. x e. dom ~~>v ( ~~>v ` x ) e. ~H
21 ffnfv 
 |-  ( ~~>v : dom ~~>v --> ~H <-> ( ~~>v Fn dom ~~>v /\ A. x e. dom ~~>v ( ~~>v ` x ) e. ~H ) )
22 14 20 21 mpbir2an 
 |-  ~~>v : dom ~~>v --> ~H