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 = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccn	⊢ Cn
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vk	⊢ 𝑘
4		vf	⊢ 𝑓
5	3	cv	⊢ 𝑘
6	5	cuni	⊢ ∪ 𝑘
7		cmap	⊢ ↑m
8	1	cv	⊢ 𝑗
9	8	cuni	⊢ ∪ 𝑗
10	6 9 7	co	⊢ ( ∪ 𝑘 ↑m ∪ 𝑗 )
11		vy	⊢ 𝑦
12	4	cv	⊢ 𝑓
13	12	ccnv	⊢ ◡ 𝑓
14	11	cv	⊢ 𝑦
15	13 14	cima	⊢ ( ◡ 𝑓 “ 𝑦 )
16	15 8	wcel	⊢ ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗
17	16 11 5	wral	⊢ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗
18	17 4 10	crab	⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 }
19	1 3 2 2 18	cmpo	⊢ ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } )
20	0 19	wceq	⊢ Cn = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } )