Definition df-toply1 21265

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.)

Assertion

Ref	Expression
df-toply1	⊢ toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))

Distinct variable group:   𝑓,𝑛

Detailed syntax breakdown of Definition df-toply1

Step	Hyp	Ref	Expression
1		ctp1 21260	. 2 class toPoly1
2		vf	. . 3 setvar 𝑓
3		cvv 3422	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		cn0 12163	. . . . 5 class ℕ0
6		c1o 8260	. . . . 5 class 1o
7		cmap 8573	. . . . 5 class ↑m
8	5, 6, 7	co 7255	. . . 4 class (ℕ0 ↑m 1o)
9		c0 4253	. . . . . 6 class ∅
10	4	cv 1538	. . . . . 6 class 𝑛
11	9, 10	cfv 6418	. . . . 5 class (𝑛‘∅)
12	2	cv 1538	. . . . 5 class 𝑓
13	11, 12	cfv 6418	. . . 4 class (𝑓‘(𝑛‘∅))
14	4, 8, 13	cmpt 5153	. . 3 class (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅)))
15	2, 3, 14	cmpt 5153	. 2 class (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))
16	1, 15	wceq 1539	1 wff toPoly1 = (𝑓 ∈ V ↦ (𝑛 ∈ (ℕ0 ↑m 1o) ↦ (𝑓‘(𝑛‘∅))))

This definition is referenced by: (None)