Definition df-toply1

Description: Define a function which maps a coefficient function for a univariate polynomial to the corresponding polynomial object. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Assertion	df-toply1	$$⊢{\mathrm{toPoly}}_1=\left(f\in \mathrm{V}⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼f\left(n\left(\varnothing \right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctp1	$$class{\mathrm{toPoly}}_1$$
1		vf	$$setvarf$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4		cn0	$$class{\mathbb{N}}_0$$
5		cmap	$$class{\uparrow }_{𝑚}$$
6		c1o	$$class{1}_{𝑜}$$
7	4 6 5	co	$$class\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
8	1	cv	$$setvarf$$
9	3	cv	$$setvarn$$
10		c0	$$class\varnothing$$
11	10 9	cfv	$$classn\left(\varnothing \right)$$
12	11 8	cfv	$$classf\left(n\left(\varnothing \right)\right)$$
13	3 7 12	cmpt	$$class\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼f\left(n\left(\varnothing \right)\right)\right)$$
14	1 2 13	cmpt	$$class\left(f\in \mathrm{V}⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼f\left(n\left(\varnothing \right)\right)\right)\right)$$
15	0 14	wceq	$$wff{\mathrm{toPoly}}_1=\left(f\in \mathrm{V}⟼\left(n\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼f\left(n\left(\varnothing \right)\right)\right)\right)$$