Metamath Proof Explorer

Theorem cncffvrn

Description: Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 1-May-2015)

Ref Expression
Assertion cncffvrn 
|- ( ( C C_ CC /\ F e. ( A -cn-> B ) ) -> ( F e. ( A -cn-> C ) <-> F : A --> C ) )

Proof

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