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	$$⊢S\subseteq ℂ\to C^n\left(S\right)Fn{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		ovex	$$⊢ℂ{\uparrow }_{𝑝𝑚}S\in \mathrm{V}$$
2	1	rabex	$$⊢\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}S\right)|\left(S{D}^{n}f\right)\left(n\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\in \mathrm{V}$$
3		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}S\right)|\left(S{D}^{n}f\right)\left(n\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)=\left(n\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}S\right)|\left(S{D}^{n}f\right)\left(n\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)$$
4	2 3	fnmpti	$$⊢\left(n\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}S\right)|\left(S{D}^{n}f\right)\left(n\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)Fn{\mathbb{N}}_0$$
5		cpnfval	$$⊢S\subseteq ℂ\to C^n\left(S\right)=\left(n\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}S\right)|\left(S{D}^{n}f\right)\left(n\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)$$
6	5	fneq1d	$$⊢S\subseteq ℂ\to \left(C^n\left(S\right)Fn{\mathbb{N}}_0\leftrightarrow \left(n\in {\mathbb{N}}_0⟼\left\{f\in \left(ℂ{\uparrow }_{𝑝𝑚}S\right)|\left(S{D}^{n}f\right)\left(n\right):\mathrm{dom}f\underset{cn}{⟶}ℂ\right\}\right)Fn{\mathbb{N}}_0\right)$$
7	4 6	mpbiri	$$⊢S\subseteq ℂ\to C^n\left(S\right)Fn{\mathbb{N}}_0$$