Metamath Proof Explorer

Definition df-mvr

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

Ref Expression
Assertion df-mvr ⊢ mVar = i ∈ V , r ∈ V ⟼ x ∈ i ⟼ f ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvr class mVar
1 vi setvar i
2 cvv class V
3 vr setvar r
4 vx setvar x
5 1 cv setvar i
6 vf setvar f
7 vh setvar h
8 cn0 class ℕ 0
9 cmap class ↑ 𝑚
10 8 5 9 co class ℕ 0 i
11 7 cv setvar h
12 11 ccnv class h -1
13 cn class ℕ
14 12 13 cima class h -1 ℕ
15 cfn class Fin
16 14 15 wcel wff h -1 ℕ ∈ Fin
17 16 7 10 crab class h ∈ ℕ 0 i | h -1 ℕ ∈ Fin
18 6 cv setvar f
19 vy setvar y
20 19 cv setvar y
21 4 cv setvar x
22 20 21 wceq wff y = x
23 c1 class 1
24 cc0 class 0
25 22 23 24 cif class if y = x 1 0
26 19 5 25 cmpt class y ∈ i ⟼ if y = x 1 0
27 18 26 wceq wff f = y ∈ i ⟼ if y = x 1 0
28 cur class 1 r
29 3 cv setvar r
30 29 28 cfv class 1 r
31 c0g class 0 𝑔
32 29 31 cfv class 0 r
33 27 30 32 cif class if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r
34 6 17 33 cmpt class f ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r
35 4 5 34 cmpt class x ∈ i ⟼ f ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r
36 1 3 2 2 35 cmpo class i ∈ V , r ∈ V ⟼ x ∈ i ⟼ f ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r
37 0 36 wceq wff mVar = i ∈ V , r ∈ V ⟼ x ∈ i ⟼ f ∈ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin ⟼ if f = y ∈ i ⟼ if y = x 1 0 1 r 0 r