Metamath Proof Explorer


Definition df-cn

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 for the predicate form. (Contributed by NM, 17-Oct-2006)

Ref Expression
Assertion df-cn
|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccn
 |-  Cn
1 vj
 |-  j
2 ctop
 |-  Top
3 vk
 |-  k
4 vf
 |-  f
5 3 cv
 |-  k
6 5 cuni
 |-  U. k
7 cmap
 |-  ^m
8 1 cv
 |-  j
9 8 cuni
 |-  U. j
10 6 9 7 co
 |-  ( U. k ^m U. j )
11 vy
 |-  y
12 4 cv
 |-  f
13 12 ccnv
 |-  `' f
14 11 cv
 |-  y
15 13 14 cima
 |-  ( `' f " y )
16 15 8 wcel
 |-  ( `' f " y ) e. j
17 16 11 5 wral
 |-  A. y e. k ( `' f " y ) e. j
18 17 4 10 crab
 |-  { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j }
19 1 3 2 2 18 cmpo
 |-  ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
20 0 19 wceq
 |-  Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )