Metamath Proof Explorer

Theorem elcncf1di

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

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

Proof

Step	Hyp	Ref	Expression
1		elcncf1d.1	\|- ( ph -> F : A --> B )
2		elcncf1d.2	\|- ( ph -> ( ( x e. A /\ y e. RR+ ) -> Z e. RR+ ) )
3		elcncf1d.3	\|- ( ph -> ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) )
4	2	imp	\|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> Z e. RR+ )
5		an32	\|- ( ( ( x e. A /\ w e. A ) /\ y e. RR+ ) <-> ( ( x e. A /\ y e. RR+ ) /\ w e. A ) )
6	5	bianass	\|- ( ( ph /\ ( ( x e. A /\ w e. A ) /\ y e. RR+ ) ) <-> ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ w e. A ) )
7	3	imp	\|- ( ( ph /\ ( ( x e. A /\ w e. A ) /\ y e. RR+ ) ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
8	6 7	sylbir	\|- ( ( ( ph /\ ( x e. A /\ y e. RR+ ) ) /\ w e. A ) -> ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
9	8	ralrimiva	\|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> A. w e. A ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
10		breq2	\|- ( z = Z -> ( ( abs ` ( x - w ) ) < z <-> ( abs ` ( x - w ) ) < Z ) )
11	10	rspceaimv	\|- ( ( Z e. RR+ /\ A. w e. A ( ( abs ` ( x - w ) ) < Z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) -> E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
12	4 9 11	syl2anc	\|- ( ( ph /\ ( x e. A /\ y e. RR+ ) ) -> E. z e. RR+ A. w e. A ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
13	12	ralrimivva	\|- ( ph -> 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 ) )
14	1 13	jca	\|- ( ph -> ( 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 ) ) )
15		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 ) ) ) )
16	14 15	syl5ibrcom	\|- ( ph -> ( ( A C_ CC /\ B C_ CC ) -> F e. ( A -cn-> B ) ) )