Detailed syntax breakdown of Definition df-oppg
Step | Hyp | Ref
| Expression |
1 | | coppg 18413 |
. 2
class
oppg |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3495 |
. . 3
class
V |
4 | 2 | cv 1527 |
. . . 4
class 𝑤 |
5 | | cnx 16470 |
. . . . . 6
class
ndx |
6 | | cplusg 16555 |
. . . . . 6
class
+g |
7 | 5, 6 | cfv 6349 |
. . . . 5
class
(+g‘ndx) |
8 | 4, 6 | cfv 6349 |
. . . . . 6
class
(+g‘𝑤) |
9 | 8 | ctpos 7882 |
. . . . 5
class tpos
(+g‘𝑤) |
10 | 7, 9 | cop 4565 |
. . . 4
class
〈(+g‘ndx), tpos (+g‘𝑤)〉 |
11 | | csts 16471 |
. . . 4
class
sSet |
12 | 4, 10, 11 | co 7145 |
. . 3
class (𝑤 sSet
〈(+g‘ndx), tpos (+g‘𝑤)〉) |
13 | 2, 3, 12 | cmpt 5138 |
. 2
class (𝑤 ∈ V ↦ (𝑤 sSet
〈(+g‘ndx), tpos (+g‘𝑤)〉)) |
14 | 1, 13 | wceq 1528 |
1
wff
oppg = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), tpos
(+g‘𝑤)〉)) |