Definition df-mvr 19758

Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)

Assertion

Ref	Expression
df-mvr	⊢ mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))))

Distinct variable group:   𝑓,ℎ,𝑖,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mvr

Step	Hyp	Ref	Expression
1		cmvr 19753	. 2 class mVar
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3398	. . 3 class V
5		vx	. . . 4 setvar 𝑥
6	2	cv 1600	. . . 4 class 𝑖
7		vf	. . . . 5 setvar 𝑓
8		vh	. . . . . . . . . 10 setvar ℎ
9	8	cv 1600	. . . . . . . . 9 class ℎ
10	9	ccnv 5356	. . . . . . . 8 class ◡ℎ
11		cn 11378	. . . . . . . 8 class ℕ
12	10, 11	cima 5360	. . . . . . 7 class (◡ℎ “ ℕ)
13		cfn 8243	. . . . . . 7 class Fin
14	12, 13	wcel 2107	. . . . . 6 wff (◡ℎ “ ℕ) ∈ Fin
15		cn0 11646	. . . . . . 7 class ℕ0
16		cmap 8142	. . . . . . 7 class ↑𝑚
17	15, 6, 16	co 6924	. . . . . 6 class (ℕ0 ↑𝑚 𝑖)
18	14, 8, 17	crab 3094	. . . . 5 class {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin}
19	7	cv 1600	. . . . . . 7 class 𝑓
20		vy	. . . . . . . 8 setvar 𝑦
21	20, 5	weq 2005	. . . . . . . . 9 wff 𝑦 = 𝑥
22		c1 10275	. . . . . . . . 9 class 1
23		cc0 10274	. . . . . . . . 9 class 0
24	21, 22, 23	cif 4307	. . . . . . . 8 class if(𝑦 = 𝑥, 1, 0)
25	20, 6, 24	cmpt 4967	. . . . . . 7 class (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
26	19, 25	wceq 1601	. . . . . 6 wff 𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
27	3	cv 1600	. . . . . . 7 class 𝑟
28		cur 18892	. . . . . . 7 class 1r
29	27, 28	cfv 6137	. . . . . 6 class (1r‘𝑟)
30		c0g 16490	. . . . . . 7 class 0g
31	27, 30	cfv 6137	. . . . . 6 class (0g‘𝑟)
32	26, 29, 31	cif 4307	. . . . 5 class if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))
33	7, 18, 32	cmpt 4967	. . . 4 class (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))
34	5, 6, 33	cmpt 4967	. . 3 class (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))))
35	2, 3, 4, 4, 34	cmpt2 6926	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))))
36	1, 35	wceq 1601	1 wff mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0 ↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))))

This definition is referenced by:  mvrfval  19821  vr1val  19962