Definition df-cnp

Description: Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of Munkres p. 107. (Contributed by NM, 17-Oct-2006)

	Ref	Expression
Assertion	df-cnp	⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccnp	⊢ CnP
1		vj	⊢ 𝑗
2		ctop	⊢ Top
3		vk	⊢ 𝑘
4		vx	⊢ 𝑥
5	1	cv	⊢ 𝑗
6	5	cuni	⊢ ∪ 𝑗
7		vf	⊢ 𝑓
8	3	cv	⊢ 𝑘
9	8	cuni	⊢ ∪ 𝑘
10		cmap	⊢ ↑m
11	9 6 10	co	⊢ ( ∪ 𝑘 ↑m ∪ 𝑗 )
12		vy	⊢ 𝑦
13	7	cv	⊢ 𝑓
14	4	cv	⊢ 𝑥
15	14 13	cfv	⊢ ( 𝑓 ‘ 𝑥 )
16	12	cv	⊢ 𝑦
17	15 16	wcel	⊢ ( 𝑓 ‘ 𝑥 ) ∈ 𝑦
18		vg	⊢ 𝑔
19	18	cv	⊢ 𝑔
20	14 19	wcel	⊢ 𝑥 ∈ 𝑔
21	13 19	cima	⊢ ( 𝑓 “ 𝑔 )
22	21 16	wss	⊢ ( 𝑓 “ 𝑔 ) ⊆ 𝑦
23	20 22	wa	⊢ ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 )
24	23 18 5	wrex	⊢ ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 )
25	17 24	wi	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) )
26	25 12 8	wral	⊢ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) )
27	26 7 11	crab	⊢ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) }
28	4 6 27	cmpt	⊢ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } )
29	1 3 2 2 28	cmpo	⊢ ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )
30	0 29	wceq	⊢ CnP = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑔 ∈ 𝑗 ( 𝑥 ∈ 𝑔 ∧ ( 𝑓 “ 𝑔 ) ⊆ 𝑦 ) ) } ) )