Theorem elcncf1ii

Description: Membership in the set of continuous complex functions from A to B . (Contributed by Paul Chapman, 26-Nov-2007)

	Ref	Expression
Hypotheses	elcncf1i.1	|- F : A --> B
	elcncf1i.2	|- ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ )
	elcncf1i.3	|- ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
Assertion	elcncf1ii	|- ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) )

Proof

Step	Hyp	Ref	Expression
1		elcncf1i.1	|- F : A --> B
2		elcncf1i.2	|- ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ )
3		elcncf1i.3	|- ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
4	1	a1i	|- ( T. -> F : A --> B )
5	2	a1i	|- ( T. -> ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ ) )
6	3	a1i	|- ( T. -> ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) )
7	4 5 6	elcncf1di	|- ( T. -> ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) ) )
8	7	mptru	|- ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) )