Theorem cpnfval

Description: Condition for n-times continuous differentiability. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	cpnfval	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2	1	elpw2	⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
3		oveq2	⊢ ( 𝑠 = 𝑆 → ( ℂ ↑pm 𝑠 ) = ( ℂ ↑pm 𝑆 ) )
4		oveq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 D𝑛 𝑓 ) = ( 𝑆 D𝑛 𝑓 ) )
5	4	fveq1d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑛 ) = ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) )
6	5	eleq1d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) ↔ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) ) )
7	3 6	rabeqbidv	⊢ ( 𝑠 = 𝑆 → { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } = { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
8	7	mpteq2dv	⊢ ( 𝑠 = 𝑆 → ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
9		df-cpn	⊢ 𝓑C𝑛 = ( 𝑠 ∈ 𝒫 ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ∣ ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
10		nn0ex	⊢ ℕ0 ∈ V
11	10	mptex	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) ∈ V
12	8 9 11	fvmpt	⊢ ( 𝑆 ∈ 𝒫 ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
13	2 12	sylbir	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )