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

Metamath Proof Explorer

Theorem iscn2

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 Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses iscn.1 
|- X = U. J
iscn.2 
|- Y = U. K
Assertion iscn2 
|- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )

Proof

Step Hyp Ref Expression
1 iscn.1 
 |-  X = U. J
2 iscn.2 
 |-  Y = U. K
3 df-cn 
 |-  Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
4 3 elmpocl 
 |-  ( F e. ( J Cn K ) -> ( J e. Top /\ K e. Top ) )
5 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
6 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
7 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 ) ) )
8 5 6 7 syl2anb 
 |-  ( ( J e. Top /\ K e. Top ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
9 4 8 biadanii 
 |-  ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )