Detailed syntax breakdown of Definition df-mpl
Step | Hyp | Ref
| Expression |
1 | | cmpl 20865 |
. 2
class
mPoly |
2 | | vi |
. . 3
setvar 𝑖 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cvv 3408 |
. . 3
class
V |
5 | | vw |
. . . 4
setvar 𝑤 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑖 |
7 | 3 | cv 1542 |
. . . . 5
class 𝑟 |
8 | | cmps 20863 |
. . . . 5
class
mPwSer |
9 | 6, 7, 8 | co 7213 |
. . . 4
class (𝑖 mPwSer 𝑟) |
10 | 5 | cv 1542 |
. . . . 5
class 𝑤 |
11 | | vf |
. . . . . . . 8
setvar 𝑓 |
12 | 11 | cv 1542 |
. . . . . . 7
class 𝑓 |
13 | | c0g 16944 |
. . . . . . . 8
class
0g |
14 | 7, 13 | cfv 6380 |
. . . . . . 7
class
(0g‘𝑟) |
15 | | cfsupp 8985 |
. . . . . . 7
class
finSupp |
16 | 12, 14, 15 | wbr 5053 |
. . . . . 6
wff 𝑓 finSupp
(0g‘𝑟) |
17 | | cbs 16760 |
. . . . . . 7
class
Base |
18 | 10, 17 | cfv 6380 |
. . . . . 6
class
(Base‘𝑤) |
19 | 16, 11, 18 | crab 3065 |
. . . . 5
class {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)} |
20 | | cress 16784 |
. . . . 5
class
↾s |
21 | 10, 19, 20 | co 7213 |
. . . 4
class (𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}) |
22 | 5, 9, 21 | csb 3811 |
. . 3
class
⦋(𝑖
mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}) |
23 | 2, 3, 4, 4, 22 | cmpo 7215 |
. 2
class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})) |
24 | 1, 23 | wceq 1543 |
1
wff mPoly =
(𝑖 ∈ V, 𝑟 ∈ V ↦
⦋(𝑖 mPwSer
𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})) |