Step | Hyp | Ref
| Expression |
1 | | cpws 17399 |
. 2
class
βs |
2 | | vr |
. . 3
setvar π |
3 | | vi |
. . 3
setvar π |
4 | | cvv 3473 |
. . 3
class
V |
5 | 2 | cv 1539 |
. . . . 5
class π |
6 | | csca 17207 |
. . . . 5
class
Scalar |
7 | 5, 6 | cfv 6543 |
. . . 4
class
(Scalarβπ) |
8 | 3 | cv 1539 |
. . . . 5
class π |
9 | 5 | csn 4628 |
. . . . 5
class {π} |
10 | 8, 9 | cxp 5674 |
. . . 4
class (π Γ {π}) |
11 | | cprds 17398 |
. . . 4
class Xs |
12 | 7, 10, 11 | co 7412 |
. . 3
class
((Scalarβπ)Xs(π Γ {π})) |
13 | 2, 3, 4, 4, 12 | cmpo 7414 |
. 2
class (π β V, π β V β¦ ((Scalarβπ)Xs(π Γ {π}))) |
14 | 1, 13 | wceq 1540 |
1
wff
βs = (π β V, π β V β¦ ((Scalarβπ)Xs(π Γ {π}))) |