Metamath Proof Explorer


Theorem rlimpm

Description: Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014)

Ref Expression
Assertion rlimpm
|- ( F ~~>r A -> F e. ( CC ^pm RR ) )

Proof

Step Hyp Ref Expression
1 df-rlim
 |-  ~~>r = { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) }
2 opabssxp
 |-  { <. f , x >. | ( ( f e. ( CC ^pm RR ) /\ x e. CC ) /\ A. y e. RR+ E. z e. RR A. w e. dom f ( z <_ w -> ( abs ` ( ( f ` w ) - x ) ) < y ) ) } C_ ( ( CC ^pm RR ) X. CC )
3 1 2 eqsstri
 |-  ~~>r C_ ( ( CC ^pm RR ) X. CC )
4 dmss
 |-  ( ~~>r C_ ( ( CC ^pm RR ) X. CC ) -> dom ~~>r C_ dom ( ( CC ^pm RR ) X. CC ) )
5 3 4 ax-mp
 |-  dom ~~>r C_ dom ( ( CC ^pm RR ) X. CC )
6 dmxpss
 |-  dom ( ( CC ^pm RR ) X. CC ) C_ ( CC ^pm RR )
7 5 6 sstri
 |-  dom ~~>r C_ ( CC ^pm RR )
8 rlimrel
 |-  Rel ~~>r
9 8 releldmi
 |-  ( F ~~>r A -> F e. dom ~~>r )
10 7 9 sselid
 |-  ( F ~~>r A -> F e. ( CC ^pm RR ) )