Detailed syntax breakdown of Definition df-scaf
Step | Hyp | Ref
| Expression |
1 | | cscaf 20133 |
. 2
class
·sf |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | cvv 3433 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | | vy |
. . . 4
setvar 𝑦 |
6 | 2 | cv 1538 |
. . . . . 6
class 𝑔 |
7 | | csca 16974 |
. . . . . 6
class
Scalar |
8 | 6, 7 | cfv 6437 |
. . . . 5
class
(Scalar‘𝑔) |
9 | | cbs 16921 |
. . . . 5
class
Base |
10 | 8, 9 | cfv 6437 |
. . . 4
class
(Base‘(Scalar‘𝑔)) |
11 | 6, 9 | cfv 6437 |
. . . 4
class
(Base‘𝑔) |
12 | 4 | cv 1538 |
. . . . 5
class 𝑥 |
13 | 5 | cv 1538 |
. . . . 5
class 𝑦 |
14 | | cvsca 16975 |
. . . . . 6
class
·𝑠 |
15 | 6, 14 | cfv 6437 |
. . . . 5
class (
·𝑠 ‘𝑔) |
16 | 12, 13, 15 | co 7284 |
. . . 4
class (𝑥(
·𝑠 ‘𝑔)𝑦) |
17 | 4, 5, 10, 11, 16 | cmpo 7286 |
. . 3
class (𝑥 ∈
(Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠
‘𝑔)𝑦)) |
18 | 2, 3, 17 | cmpt 5158 |
. 2
class (𝑔 ∈ V ↦ (𝑥 ∈
(Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠
‘𝑔)𝑦))) |
19 | 1, 18 | wceq 1539 |
1
wff
·sf = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘(Scalar‘𝑔)), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥( ·𝑠
‘𝑔)𝑦))) |