Detailed syntax breakdown of Definition df-scmat
Step | Hyp | Ref
| Expression |
1 | | cscmat 21386 |
. 2
class
ScMat |
2 | | vn |
. . 3
setvar 𝑛 |
3 | | vr |
. . 3
setvar 𝑟 |
4 | | cfn 8626 |
. . 3
class
Fin |
5 | | cvv 3408 |
. . 3
class
V |
6 | | va |
. . . 4
setvar 𝑎 |
7 | 2 | cv 1542 |
. . . . 5
class 𝑛 |
8 | 3 | cv 1542 |
. . . . 5
class 𝑟 |
9 | | cmat 21304 |
. . . . 5
class
Mat |
10 | 7, 8, 9 | co 7213 |
. . . 4
class (𝑛 Mat 𝑟) |
11 | | vm |
. . . . . . . 8
setvar 𝑚 |
12 | 11 | cv 1542 |
. . . . . . 7
class 𝑚 |
13 | | vc |
. . . . . . . . 9
setvar 𝑐 |
14 | 13 | cv 1542 |
. . . . . . . 8
class 𝑐 |
15 | 6 | cv 1542 |
. . . . . . . . 9
class 𝑎 |
16 | | cur 19516 |
. . . . . . . . 9
class
1r |
17 | 15, 16 | cfv 6380 |
. . . . . . . 8
class
(1r‘𝑎) |
18 | | cvsca 16806 |
. . . . . . . . 9
class
·𝑠 |
19 | 15, 18 | cfv 6380 |
. . . . . . . 8
class (
·𝑠 ‘𝑎) |
20 | 14, 17, 19 | co 7213 |
. . . . . . 7
class (𝑐(
·𝑠 ‘𝑎)(1r‘𝑎)) |
21 | 12, 20 | wceq 1543 |
. . . . . 6
wff 𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎)) |
22 | | cbs 16760 |
. . . . . . 7
class
Base |
23 | 8, 22 | cfv 6380 |
. . . . . 6
class
(Base‘𝑟) |
24 | 21, 13, 23 | wrex 3062 |
. . . . 5
wff
∃𝑐 ∈
(Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎)) |
25 | 15, 22 | cfv 6380 |
. . . . 5
class
(Base‘𝑎) |
26 | 24, 11, 25 | crab 3065 |
. . . 4
class {𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))} |
27 | 6, 10, 26 | csb 3811 |
. . 3
class
⦋(𝑛
Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))} |
28 | 2, 3, 4, 5, 27 | cmpo 7215 |
. 2
class (𝑛 ∈ Fin, 𝑟 ∈ V ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))}) |
29 | 1, 28 | wceq 1543 |
1
wff ScMat =
(𝑛 ∈ Fin, 𝑟 ∈ V ↦
⦋(𝑛 Mat 𝑟) / 𝑎⦌{𝑚 ∈ (Base‘𝑎) ∣ ∃𝑐 ∈ (Base‘𝑟)𝑚 = (𝑐( ·𝑠
‘𝑎)(1r‘𝑎))}) |