Definition df-cn 14918

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 14927 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

Step	Hyp	Ref	Expression
1		ccn 14915	. 2 class Cn
2		vj	. . 3 setvar 𝑗
3		vk	. . 3 setvar 𝑘
4		ctop 14727	. . 3 class Top
5		vf	. . . . . . . . 9 setvar 𝑓
6	5	cv 1396	. . . . . . . 8 class 𝑓
7	6	ccnv 4724	. . . . . . 7 class ◡𝑓
8		vy	. . . . . . . 8 setvar 𝑦
9	8	cv 1396	. . . . . . 7 class 𝑦
10	7, 9	cima 4728	. . . . . 6 class (◡𝑓 “ 𝑦)
11	2	cv 1396	. . . . . 6 class 𝑗
12	10, 11	wcel 2202	. . . . 5 wff (◡𝑓 “ 𝑦) ∈ 𝑗
13	3	cv 1396	. . . . 5 class 𝑘
14	12, 8, 13	wral 2510	. . . 4 wff ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗
15	13	cuni 3893	. . . . 5 class ∪ 𝑘
16	11	cuni 3893	. . . . 5 class ∪ 𝑗
17		cmap 6817	. . . . 5 class ↑𝑚
18	15, 16, 17	co 6018	. . . 4 class (∪ 𝑘 ↑𝑚 ∪ 𝑗)
19	14, 5, 18	crab 2514	. . 3 class {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗}
20	2, 3, 4, 4, 19	cmpo 6020	. 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗})
21	1, 20	wceq 1397	1 wff Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑𝑚 ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗})

This definition is referenced by:  cnfval  14924  iscn2  14930  ishmeo  15034