df-coe1

Description: Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015)

		Ref	Expression
	Assertion	df-coe1	$⊢ {coe}_{1} = (f \in V ⟼ (n \in ℕ_{0} ⟼ f (1_{𝑜} \times \{n\})))$

Step	Hyp	Ref	Expression
0		cco1	$class {coe}_{1}$
1		vf	$setvar f$
2		cvv	$class V$
3		vn	$setvar n$
4		cn0	$class ℕ_{0}$
5	1	cv	$setvar f$
6		c1o	$class 1_{𝑜}$
7	3	cv	$setvar n$
8	7	csn	$class \{n\}$
9	6 8	cxp	$class (1_{𝑜} \times \{n\})$
10	9 5	cfv	$class f (1_{𝑜} \times \{n\})$
11	3 4 10	cmpt	$class (n \in ℕ_{0} ⟼ f (1_{𝑜} \times \{n\}))$
12	1 2 11	cmpt	$class (f \in V ⟼ (n \in ℕ_{0} ⟼ f (1_{𝑜} \times \{n\})))$
13	0 12	wceq	$wff {coe}_{1} = (f \in V ⟼ (n \in ℕ_{0} ⟼ f (1_{𝑜} \times \{n\})))$

Metamath Proof Explorer