MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cn Unicode version

Definition df-cn 16919
Description: Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 16927 for the predicate form. (Contributed by NM, 17-Oct-2006.)
Assertion
Ref Expression
df-cn  |-  Cn  =  ( j  e.  Top ,  k  e.  Top  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( `' f
" y )  e.  j } )
Distinct variable group:    j, k, f, y

Detailed syntax breakdown of Definition df-cn
StepHypRef Expression
1 ccn 16916 . 2  class  Cn
2 vj . . 3  set  j
3 vk . . 3  set  k
4 ctop 16593 . . 3  class  Top
5 vf . . . . . . . . 9  set  f
65cv 1618 . . . . . . . 8  class  f
76ccnv 4660 . . . . . . 7  class  `' f
8 vy . . . . . . . 8  set  y
98cv 1618 . . . . . . 7  class  y
107, 9cima 4664 . . . . . 6  class  ( `' f " y )
112cv 1618 . . . . . 6  class  j
1210, 11wcel 1621 . . . . 5  wff  ( `' f " y )  e.  j
133cv 1618 . . . . 5  class  k
1412, 8, 13wral 2518 . . . 4  wff  A. y  e.  k  ( `' f " y )  e.  j
1513cuni 3801 . . . . 5  class  U. k
1611cuni 3801 . . . . 5  class  U. j
17 cmap 6740 . . . . 5  class  ^m
1815, 16, 17co 5792 . . . 4  class  ( U. k  ^m  U. j )
1914, 5, 18crab 2522 . . 3  class  { f  e.  ( U. k  ^m  U. j )  | 
A. y  e.  k  ( `' f "
y )  e.  j }
202, 3, 4, 4, 19cmpt2 5794 . 2  class  ( j  e.  Top ,  k  e.  Top  |->  { f  e.  ( U. k  ^m  U. j )  | 
A. y  e.  k  ( `' f "
y )  e.  j } )
211, 20wceq 1619 1  wff  Cn  =  ( j  e.  Top ,  k  e.  Top  |->  { f  e.  ( U. k  ^m  U. j )  |  A. y  e.  k  ( `' f
" y )  e.  j } )
Colors of variables: wff set class
This definition is referenced by:  cnfval  16925  iscn2  16930
  Copyright terms: Public domain W3C validator