Theorem fncpn

Description: The C^n object is a function. (Contributed by Stefan O'Rear, 16-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	fncpn	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ℂ ↑pm 𝑆 ) ∈ V
2	1	rabex	⊢ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ∈ V
3		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } )
4	2 3	fnmpti	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) Fn ℕ0
5		cpnfval	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) )
6	5	fneq1d	⊢ ( 𝑆 ⊆ ℂ → ( ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 ↔ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( ℂ ↑pm 𝑆 ) ∣ ( ( 𝑆 D𝑛 𝑓 ) ‘ 𝑛 ) ∈ ( dom 𝑓 –cn→ ℂ ) } ) Fn ℕ0 ) )
7	4 6	mpbiri	⊢ ( 𝑆 ⊆ ℂ → ( 𝓑C𝑛 ‘ 𝑆 ) Fn ℕ0 )