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

Definition df-cn 20841
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 20849 for the predicate form. (Contributed by NM, 17-Oct-2006.)
Assertion
Ref Expression
df-cn Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 (𝑓𝑦) ∈ 𝑗})
Distinct variable group:   𝑗,𝑘,𝑓,𝑦

Detailed syntax breakdown of Definition df-cn
StepHypRef Expression
1 ccn 20838 . 2 class Cn
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 20517 . . 3 class Top
5 vf . . . . . . . . 9 setvar 𝑓
65cv 1474 . . . . . . . 8 class 𝑓
76ccnv 5037 . . . . . . 7 class 𝑓
8 vy . . . . . . . 8 setvar 𝑦
98cv 1474 . . . . . . 7 class 𝑦
107, 9cima 5041 . . . . . 6 class (𝑓𝑦)
112cv 1474 . . . . . 6 class 𝑗
1210, 11wcel 1977 . . . . 5 wff (𝑓𝑦) ∈ 𝑗
133cv 1474 . . . . 5 class 𝑘
1412, 8, 13wral 2896 . . . 4 wff 𝑦𝑘 (𝑓𝑦) ∈ 𝑗
1513cuni 4372 . . . . 5 class 𝑘
1611cuni 4372 . . . . 5 class 𝑗
17 cmap 7744 . . . . 5 class 𝑚
1815, 16, 17co 6549 . . . 4 class ( 𝑘𝑚 𝑗)
1914, 5, 18crab 2900 . . 3 class {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 (𝑓𝑦) ∈ 𝑗}
202, 3, 4, 4, 19cmpt2 6551 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 (𝑓𝑦) ∈ 𝑗})
211, 20wceq 1475 1 wff Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑦𝑘 (𝑓𝑦) ∈ 𝑗})
Colors of variables: wff setvar class
This definition is referenced by:  cnfval  20847  iscn2  20852
  Copyright terms: Public domain W3C validator