Step |
Hyp |
Ref |
Expression |
1 |
|
elcncf |
|- ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) ) ) |
2 |
|
simplll |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> A C_ CC ) |
3 |
|
simprl |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> x e. A ) |
4 |
2 3
|
sseldd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> x e. CC ) |
5 |
|
simprr |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> w e. A ) |
6 |
2 5
|
sseldd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> w e. CC ) |
7 |
4 6
|
abssubd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( abs ` ( x - w ) ) = ( abs ` ( w - x ) ) ) |
8 |
7
|
breq1d |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( abs ` ( x - w ) ) < z <-> ( abs ` ( w - x ) ) < z ) ) |
9 |
|
simpllr |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> B C_ CC ) |
10 |
|
simplr |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> F : A --> B ) |
11 |
10 3
|
ffvelrnd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( F ` x ) e. B ) |
12 |
9 11
|
sseldd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( F ` x ) e. CC ) |
13 |
10 5
|
ffvelrnd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( F ` w ) e. B ) |
14 |
9 13
|
sseldd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( F ` w ) e. CC ) |
15 |
12 14
|
abssubd |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) = ( abs ` ( ( F ` w ) - ( F ` x ) ) ) ) |
16 |
15
|
breq1d |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y <-> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) |
17 |
8 16
|
imbi12d |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ ( x e. A /\ w e. A ) ) -> ( ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) <-> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) |
18 |
17
|
anassrs |
|- ( ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ x e. A ) /\ w e. A ) -> ( ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) <-> ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) |
19 |
18
|
ralbidva |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ x e. A ) -> ( A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) <-> A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) |
20 |
19
|
rexbidv |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ x e. A ) -> ( E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) <-> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) |
21 |
20
|
ralbidv |
|- ( ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) /\ x e. A ) -> ( A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) <-> A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) |
22 |
21
|
ralbidva |
|- ( ( ( A C_ CC /\ B C_ CC ) /\ F : A --> B ) -> ( A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) <-> A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) |
23 |
22
|
pm5.32da |
|- ( ( A C_ CC /\ B C_ CC ) -> ( ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) ) |
24 |
1 23
|
bitrd |
|- ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F : A --> B /\ A. x e. A A. y e. RR+ E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) ) ) |