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 )