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 sseldi 
 |-  ( F ~~>r A -> F e. ( CC ^pm RR ) )