Step | Hyp | Ref
| Expression |
1 | | coppg 19250 |
. 2
class
oppg |
2 | | vw |
. . 3
setvar π€ |
3 | | cvv 3472 |
. . 3
class
V |
4 | 2 | cv 1538 |
. . . 4
class π€ |
5 | | cnx 17130 |
. . . . . 6
class
ndx |
6 | | cplusg 17201 |
. . . . . 6
class
+g |
7 | 5, 6 | cfv 6542 |
. . . . 5
class
(+gβndx) |
8 | 4, 6 | cfv 6542 |
. . . . . 6
class
(+gβπ€) |
9 | 8 | ctpos 8212 |
. . . . 5
class tpos
(+gβπ€) |
10 | 7, 9 | cop 4633 |
. . . 4
class
β¨(+gβndx), tpos (+gβπ€)β© |
11 | | csts 17100 |
. . . 4
class
sSet |
12 | 4, 10, 11 | co 7411 |
. . 3
class (π€ sSet
β¨(+gβndx), tpos (+gβπ€)β©) |
13 | 2, 3, 12 | cmpt 5230 |
. 2
class (π€ β V β¦ (π€ sSet
β¨(+gβndx), tpos (+gβπ€)β©)) |
14 | 1, 13 | wceq 1539 |
1
wff
oppg = (π€ β V β¦ (π€ sSet β¨(+gβndx), tpos
(+gβπ€)β©)) |