Description: Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | df-resv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cresv | |
|
1 | vw | |
|
2 | cvv | |
|
3 | vx | |
|
4 | cbs | |
|
5 | csca | |
|
6 | 1 | cv | |
7 | 6 5 | cfv | |
8 | 7 4 | cfv | |
9 | 3 | cv | |
10 | 8 9 | wss | |
11 | csts | |
|
12 | cnx | |
|
13 | 12 5 | cfv | |
14 | cress | |
|
15 | 7 9 14 | co | |
16 | 13 15 | cop | |
17 | 6 16 11 | co | |
18 | 10 6 17 | cif | |
19 | 1 3 2 2 18 | cmpo | |
20 | 0 19 | wceq | |