This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncff

Description: A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008) (Revised by Mario Carneiro, 25-Aug-2014)

Ref Expression
Assertion cncff 
|- ( F e. ( A -cn-> B ) -> F : A --> B )

Proof

Step Hyp Ref Expression
1 cncfrss 
 |-  ( F e. ( A -cn-> B ) -> A C_ CC )
2 cncfrss2 
 |-  ( F e. ( A -cn-> B ) -> B C_ CC )
3 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 ) ) ) )
4 1 2 3 syl2anc 
 |-  ( F e. ( A -cn-> B ) -> ( 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 ) ) ) )
5 4 ibi 
 |-  ( 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 ) ) )
6 5 simpld 
 |-  ( F e. ( A -cn-> B ) -> F : A --> B )