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

Definition df-cn 20243
 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 20251 for the predicate form. (Contributed by NM, 17-Oct-2006.)
Assertion
Ref Expression
df-cn
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-cn
StepHypRef Expression
1 ccn 20240 . 2
2 vj . . 3
3 vk . . 3
4 ctop 19917 . . 3
5 vf . . . . . . . . 9
65cv 1443 . . . . . . . 8
76ccnv 4833 . . . . . . 7
8 vy . . . . . . . 8
98cv 1443 . . . . . . 7
107, 9cima 4837 . . . . . 6
112cv 1443 . . . . . 6
1210, 11wcel 1887 . . . . 5
133cv 1443 . . . . 5
1412, 8, 13wral 2737 . . . 4
1513cuni 4198 . . . . 5
1611cuni 4198 . . . . 5
17 cmap 7472 . . . . 5
1815, 16, 17co 6290 . . . 4
1914, 5, 18crab 2741 . . 3
202, 3, 4, 4, 19cmpt2 6292 . 2
211, 20wceq 1444 1
 Colors of variables: wff setvar class This definition is referenced by:  cnfval  20249  iscn2  20254
 Copyright terms: Public domain W3C validator