Detailed syntax breakdown of Definition df-resv
Step | Hyp | Ref
| Expression |
1 | | cresv 29155 |
. 2
class
↾v |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | vx |
. . 3
setvar 𝑥 |
4 | | cvv 3173 |
. . 3
class
V |
5 | 2 | cv 1474 |
. . . . . . 7
class 𝑤 |
6 | | csca 15771 |
. . . . . . 7
class
Scalar |
7 | 5, 6 | cfv 5804 |
. . . . . 6
class
(Scalar‘𝑤) |
8 | | cbs 15695 |
. . . . . 6
class
Base |
9 | 7, 8 | cfv 5804 |
. . . . 5
class
(Base‘(Scalar‘𝑤)) |
10 | 3 | cv 1474 |
. . . . 5
class 𝑥 |
11 | 9, 10 | wss 3540 |
. . . 4
wff
(Base‘(Scalar‘𝑤)) ⊆ 𝑥 |
12 | | cnx 15692 |
. . . . . . 7
class
ndx |
13 | 12, 6 | cfv 5804 |
. . . . . 6
class
(Scalar‘ndx) |
14 | | cress 15696 |
. . . . . . 7
class
↾s |
15 | 7, 10, 14 | co 6549 |
. . . . . 6
class
((Scalar‘𝑤)
↾s 𝑥) |
16 | 13, 15 | cop 4131 |
. . . . 5
class
〈(Scalar‘ndx), ((Scalar‘𝑤) ↾s 𝑥)〉 |
17 | | csts 15693 |
. . . . 5
class
sSet |
18 | 5, 16, 17 | co 6549 |
. . . 4
class (𝑤 sSet 〈(Scalar‘ndx),
((Scalar‘𝑤)
↾s 𝑥)〉) |
19 | 11, 5, 18 | cif 4036 |
. . 3
class
if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Scalar‘ndx),
((Scalar‘𝑤)
↾s 𝑥)〉)) |
20 | 2, 3, 4, 4, 19 | cmpt2 6551 |
. 2
class (𝑤 ∈ V, 𝑥 ∈ V ↦
if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Scalar‘ndx),
((Scalar‘𝑤)
↾s 𝑥)〉))) |
21 | 1, 20 | wceq 1475 |
1
wff
↾v = (𝑤
∈ V, 𝑥 ∈ V
↦ if((Base‘(Scalar‘𝑤)) ⊆ 𝑥, 𝑤, (𝑤 sSet 〈(Scalar‘ndx),
((Scalar‘𝑤)
↾s 𝑥)〉))) |