Step |
Hyp |
Ref |
Expression |
1 |
|
rlim.1 |
|- ( ph -> F : A --> CC ) |
2 |
|
rlim.2 |
|- ( ph -> A C_ RR ) |
3 |
|
rlim.4 |
|- ( ( ph /\ z e. A ) -> ( F ` z ) = B ) |
4 |
|
rlimrel |
|- Rel ~~>r |
5 |
4
|
brrelex2i |
|- ( F ~~>r C -> C e. _V ) |
6 |
5
|
a1i |
|- ( ph -> ( F ~~>r C -> C e. _V ) ) |
7 |
|
elex |
|- ( C e. CC -> C e. _V ) |
8 |
7
|
ad2antrl |
|- ( ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) -> C e. _V ) |
9 |
8
|
a1i |
|- ( ph -> ( ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) -> C e. _V ) ) |
10 |
|
cnex |
|- CC e. _V |
11 |
|
reex |
|- RR e. _V |
12 |
|
elpm2r |
|- ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) ) |
13 |
10 11 12
|
mpanl12 |
|- ( ( F : A --> CC /\ A C_ RR ) -> F e. ( CC ^pm RR ) ) |
14 |
1 2 13
|
syl2anc |
|- ( ph -> F e. ( CC ^pm RR ) ) |
15 |
|
eleq1 |
|- ( f = F -> ( f e. ( CC ^pm RR ) <-> F e. ( CC ^pm RR ) ) ) |
16 |
|
eleq1 |
|- ( w = C -> ( w e. CC <-> C e. CC ) ) |
17 |
15 16
|
bi2anan9 |
|- ( ( f = F /\ w = C ) -> ( ( f e. ( CC ^pm RR ) /\ w e. CC ) <-> ( F e. ( CC ^pm RR ) /\ C e. CC ) ) ) |
18 |
|
simpl |
|- ( ( f = F /\ w = C ) -> f = F ) |
19 |
18
|
dmeqd |
|- ( ( f = F /\ w = C ) -> dom f = dom F ) |
20 |
|
fveq1 |
|- ( f = F -> ( f ` z ) = ( F ` z ) ) |
21 |
|
oveq12 |
|- ( ( ( f ` z ) = ( F ` z ) /\ w = C ) -> ( ( f ` z ) - w ) = ( ( F ` z ) - C ) ) |
22 |
20 21
|
sylan |
|- ( ( f = F /\ w = C ) -> ( ( f ` z ) - w ) = ( ( F ` z ) - C ) ) |
23 |
22
|
fveq2d |
|- ( ( f = F /\ w = C ) -> ( abs ` ( ( f ` z ) - w ) ) = ( abs ` ( ( F ` z ) - C ) ) ) |
24 |
23
|
breq1d |
|- ( ( f = F /\ w = C ) -> ( ( abs ` ( ( f ` z ) - w ) ) < x <-> ( abs ` ( ( F ` z ) - C ) ) < x ) ) |
25 |
24
|
imbi2d |
|- ( ( f = F /\ w = C ) -> ( ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) |
26 |
19 25
|
raleqbidv |
|- ( ( f = F /\ w = C ) -> ( A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) |
27 |
26
|
rexbidv |
|- ( ( f = F /\ w = C ) -> ( E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) |
28 |
27
|
ralbidv |
|- ( ( f = F /\ w = C ) -> ( A. x e. RR+ E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) <-> A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) |
29 |
17 28
|
anbi12d |
|- ( ( f = F /\ w = C ) -> ( ( ( f e. ( CC ^pm RR ) /\ w e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) ) <-> ( ( F e. ( CC ^pm RR ) /\ C e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) |
30 |
|
df-rlim |
|- ~~>r = { <. f , w >. | ( ( f e. ( CC ^pm RR ) /\ w e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom f ( y <_ z -> ( abs ` ( ( f ` z ) - w ) ) < x ) ) } |
31 |
29 30
|
brabga |
|- ( ( F e. ( CC ^pm RR ) /\ C e. _V ) -> ( F ~~>r C <-> ( ( F e. ( CC ^pm RR ) /\ C e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) |
32 |
|
anass |
|- ( ( ( F e. ( CC ^pm RR ) /\ C e. CC ) /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) |
33 |
31 32
|
bitrdi |
|- ( ( F e. ( CC ^pm RR ) /\ C e. _V ) -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) |
34 |
33
|
ex |
|- ( F e. ( CC ^pm RR ) -> ( C e. _V -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) ) |
35 |
14 34
|
syl |
|- ( ph -> ( C e. _V -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) ) |
36 |
6 9 35
|
pm5.21ndd |
|- ( ph -> ( F ~~>r C <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) |
37 |
14
|
biantrurd |
|- ( ph -> ( ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( F e. ( CC ^pm RR ) /\ ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) ) ) |
38 |
1
|
fdmd |
|- ( ph -> dom F = A ) |
39 |
38
|
raleqdv |
|- ( ph -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) ) |
40 |
3
|
fvoveq1d |
|- ( ( ph /\ z e. A ) -> ( abs ` ( ( F ` z ) - C ) ) = ( abs ` ( B - C ) ) ) |
41 |
40
|
breq1d |
|- ( ( ph /\ z e. A ) -> ( ( abs ` ( ( F ` z ) - C ) ) < x <-> ( abs ` ( B - C ) ) < x ) ) |
42 |
41
|
imbi2d |
|- ( ( ph /\ z e. A ) -> ( ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
43 |
42
|
ralbidva |
|- ( ph -> ( A. z e. A ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
44 |
39 43
|
bitrd |
|- ( ph -> ( A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
45 |
44
|
rexbidv |
|- ( ph -> ( E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
46 |
45
|
ralbidv |
|- ( ph -> ( A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) <-> A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) |
47 |
46
|
anbi2d |
|- ( ph -> ( ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. dom F ( y <_ z -> ( abs ` ( ( F ` z ) - C ) ) < x ) ) <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) ) |
48 |
36 37 47
|
3bitr2d |
|- ( ph -> ( F ~~>r C <-> ( C e. CC /\ A. x e. RR+ E. y e. RR A. z e. A ( y <_ z -> ( abs ` ( B - C ) ) < x ) ) ) ) |