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

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