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 ) ) |