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

Metamath Proof Explorer

Theorem iscn

Description: The predicate "the class F is a continuous function from topology J to topology K ". Definition of continuous function in Munkres p. 102. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscn 
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )

Proof

Step Hyp Ref Expression
1 cnfval 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J Cn K ) = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )
2 1 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> F e. { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } ) )
3 cnveq 
 |-  ( f = F -> `' f = `' F )
4 3 imaeq1d 
 |-  ( f = F -> ( `' f " y ) = ( `' F " y ) )
5 4 eleq1d 
 |-  ( f = F -> ( ( `' f " y ) e. J <-> ( `' F " y ) e. J ) )
6 5 ralbidv 
 |-  ( f = F -> ( A. y e. K ( `' f " y ) e. J <-> A. y e. K ( `' F " y ) e. J ) )
7 6 elrab 
 |-  ( F e. { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } <-> ( F e. ( Y ^m X ) /\ A. y e. K ( `' F " y ) e. J ) )
8 toponmax 
 |-  ( K e. ( TopOn ` Y ) -> Y e. K )
9 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
10 elmapg 
 |-  ( ( Y e. K /\ X e. J ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
11 8 9 10 syl2anr 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( Y ^m X ) <-> F : X --> Y ) )
12 11 anbi1d 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( ( F e. ( Y ^m X ) /\ A. y e. K ( `' F " y ) e. J ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
13 7 12 bitrid 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
14 2 13 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )