Detailed syntax breakdown of Definition df-decpmat
Step | Hyp | Ref
| Expression |
1 | | cdecpmat 21659 |
. 2
class
decompPMat |
2 | | vm |
. . 3
setvar 𝑚 |
3 | | vk |
. . 3
setvar 𝑘 |
4 | | cvv 3408 |
. . 3
class
V |
5 | | cn0 12090 |
. . 3
class
ℕ0 |
6 | | vi |
. . . 4
setvar 𝑖 |
7 | | vj |
. . . 4
setvar 𝑗 |
8 | 2 | cv 1542 |
. . . . . 6
class 𝑚 |
9 | 8 | cdm 5551 |
. . . . 5
class dom 𝑚 |
10 | 9 | cdm 5551 |
. . . 4
class dom dom
𝑚 |
11 | 3 | cv 1542 |
. . . . 5
class 𝑘 |
12 | 6 | cv 1542 |
. . . . . . 7
class 𝑖 |
13 | 7 | cv 1542 |
. . . . . . 7
class 𝑗 |
14 | 12, 13, 8 | co 7213 |
. . . . . 6
class (𝑖𝑚𝑗) |
15 | | cco1 21099 |
. . . . . 6
class
coe1 |
16 | 14, 15 | cfv 6380 |
. . . . 5
class
(coe1‘(𝑖𝑚𝑗)) |
17 | 11, 16 | cfv 6380 |
. . . 4
class
((coe1‘(𝑖𝑚𝑗))‘𝑘) |
18 | 6, 7, 10, 10, 17 | cmpo 7215 |
. . 3
class (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘)) |
19 | 2, 3, 4, 5, 18 | cmpo 7215 |
. 2
class (𝑚 ∈ V, 𝑘 ∈ ℕ0 ↦ (𝑖 ∈ dom dom 𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))) |
20 | 1, 19 | wceq 1543 |
1
wff decompPMat
= (𝑚 ∈ V, 𝑘 ∈ ℕ0
↦ (𝑖 ∈ dom dom
𝑚, 𝑗 ∈ dom dom 𝑚 ↦ ((coe1‘(𝑖𝑚𝑗))‘𝑘))) |