df-cpn

Description: Define the set of n -times continuously differentiable functions. (Contributed by Stefan O'Rear, 15-Nov-2014)

		Ref	Expression
	Assertion	df-cpn	⊢ 𝓑C^𝑛 = ( 𝑠 ∈ 𝒫 ℂ ↦ ( 𝑥 ∈ ℕ₀ ↦ { 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ∣ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )

Step	Hyp	Ref	Expression
0		ccpn	⊢ 𝓑C^𝑛
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3	2	cpw	⊢ 𝒫 ℂ
4		vx	⊢ 𝑥
5		cn0	⊢ ℕ₀
6		vf	⊢ 𝑓
7		cpm	⊢ ↑_pm
8	1	cv	⊢ 𝑠
9	2 8 7	co	⊢ ( ℂ ↑_pm 𝑠 )
10		cdvn	⊢ D^𝑛
11	6	cv	⊢ 𝑓
12	8 11 10	co	⊢ ( 𝑠 D^𝑛 𝑓 )
13	4	cv	⊢ 𝑥
14	13 12	cfv	⊢ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 )
15	11	cdm	⊢ dom 𝑓
16		ccncf	⊢ –cn→
17	15 2 16	co	⊢ ( dom 𝑓 –cn→ ℂ )
18	14 17	wcel	⊢ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 ) ∈ ( dom 𝑓 –cn→ ℂ )
19	18 6 9	crab	⊢ { 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ∣ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 ) ∈ ( dom 𝑓 –cn→ ℂ ) }
20	4 5 19	cmpt	⊢ ( 𝑥 ∈ ℕ₀ ↦ { 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ∣ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
21	1 3 20	cmpt	⊢ ( 𝑠 ∈ 𝒫 ℂ ↦ ( 𝑥 ∈ ℕ₀ ↦ { 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ∣ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
22	0 21	wceq	⊢ 𝓑C^𝑛 = ( 𝑠 ∈ 𝒫 ℂ ↦ ( 𝑥 ∈ ℕ₀ ↦ { 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ∣ ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑥 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )

Metamath Proof Explorer