Metamath Proof Explorer

Theorem elcncf

Description: Membership in the set of continuous complex functions from A to B . (Contributed by Paul Chapman, 11-Oct-2007) (Revised by Mario Carneiro, 9-Nov-2013)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 cncfval 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( A -cn-> B ) = { f e. ( B ^m A ) | 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 ) } )
2 1 eleq2d 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> F e. { f e. ( B ^m A ) | 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 ) } ) )
3 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
4 fveq1 
 |-  ( f = F -> ( f ` w ) = ( F ` w ) )
5 3 4 oveq12d 
 |-  ( f = F -> ( ( f ` x ) - ( f ` w ) ) = ( ( F ` x ) - ( F ` w ) ) )
6 5 fveq2d 
 |-  ( f = F -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) = ( abs ` ( ( F ` x ) - ( F ` w ) ) ) )
7 6 breq1d 
 |-  ( f = F -> ( ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y <-> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) )
8 7 imbi2d 
 |-  ( f = F -> ( ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( f ` x ) - ( f ` w ) ) ) < y ) <-> ( ( abs ` ( x - w ) ) < z -> ( abs ` ( ( F ` x ) - ( F ` w ) ) ) < y ) ) )
9 8 rexralbidv 
 |-  ( f = F -> ( E. 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 ) ) )
10 9 2ralbidv 
 |-  ( f = F -> ( 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 ) <-> 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 ) ) )
11 10 elrab 
 |-  ( F e. { f e. ( B ^m A ) | 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 ) } <-> ( F e. ( B ^m A ) /\ 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 ) ) )
12 2 11 bitrdi 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( A -cn-> B ) <-> ( F e. ( B ^m A ) /\ 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 ) ) ) )
13 cnex 
 |-  CC e. _V
14 13 ssex 
 |-  ( B C_ CC -> B e. _V )
15 13 ssex 
 |-  ( A C_ CC -> A e. _V )
16 elmapg 
 |-  ( ( B e. _V /\ A e. _V ) -> ( F e. ( B ^m A ) <-> F : A --> B ) )
17 14 15 16 syl2anr 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( F e. ( B ^m A ) <-> F : A --> B ) )
18 17 anbi1d 
 |-  ( ( A C_ CC /\ B C_ CC ) -> ( ( F e. ( B ^m A ) /\ 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 ) ) <-> ( 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 ) ) ) )
19 12 18 bitrd 
 |-  ( ( 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 ) ) ) )