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

Definition df-cn 16952
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 16960 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 16949 . 2  class  Cn
2 vj . . 3  set  j
3 vk . . 3  set  k
4 ctop 16626 . . 3  class  Top
5 vf . . . . . . . . 9  set  f
65cv 1623 . . . . . . . 8  class  f
76ccnv 4688 . . . . . . 7  class  `' f
8 vy . . . . . . . 8  set  y
98cv 1623 . . . . . . 7  class  y
107, 9cima 4692 . . . . . 6  class  ( `' f " y )
112cv 1623 . . . . . 6  class  j
1210, 11wcel 1685 . . . . 5  wff  ( `' f " y )  e.  j
133cv 1623 . . . . 5  class  k
1412, 8, 13wral 2545 . . . 4  wff  A. y  e.  k  ( `' f " y )  e.  j
1513cuni 3829 . . . . 5  class  U. k
1611cuni 3829 . . . . 5  class  U. j
17 cmap 6768 . . . . 5  class  ^m
1815, 16, 17co 5820 . . . 4  class  ( U. k  ^m  U. j )
1914, 5, 18crab 2549 . . 3  class  { f  e.  ( U. k  ^m  U. j )  | 
A. y  e.  k  ( `' f "
y )  e.  j }
202, 3, 4, 4, 19cmpt2 5822 . 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 1624 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  16958  iscn2  16963
  Copyright terms: Public domain W3C validator