Step |
Hyp |
Ref |
Expression |
1 |
|
cncfi |
|- ( ( F e. ( A -cn-> B ) /\ x e. A /\ y e. RR+ ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) |
2 |
1
|
3expb |
|- ( ( F e. ( A -cn-> B ) /\ ( x e. A /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. A ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( F ` w ) - ( F ` x ) ) ) < y ) ) |
3 |
2
|
ralrimivva |
|- ( F e. ( A -cn-> 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 ) ) |
4 |
3
|
adantl |
|- ( ( C C_ CC /\ F e. ( A -cn-> 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 ) ) |
5 |
|
cncfrss |
|- ( F e. ( A -cn-> B ) -> A C_ CC ) |
6 |
|
simpl |
|- ( ( C C_ CC /\ F e. ( A -cn-> B ) ) -> C C_ CC ) |
7 |
|
elcncf2 |
|- ( ( A C_ CC /\ C C_ CC ) -> ( F e. ( A -cn-> C ) <-> ( F : A --> C /\ 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 ) ) ) ) |
8 |
5 6 7
|
syl2an2 |
|- ( ( C C_ CC /\ F e. ( A -cn-> B ) ) -> ( F e. ( A -cn-> C ) <-> ( F : A --> C /\ 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 ) ) ) ) |
9 |
4 8
|
mpbiran2d |
|- ( ( C C_ CC /\ F e. ( A -cn-> B ) ) -> ( F e. ( A -cn-> C ) <-> F : A --> C ) ) |