Step | Hyp | Ref
| Expression |
1 | | coppr 20149 |
. 2
class
oppr |
2 | | vf |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | 2 | cv 1541 |
. . . 4
class π |
5 | | cnx 17126 |
. . . . . 6
class
ndx |
6 | | cmulr 17198 |
. . . . . 6
class
.r |
7 | 5, 6 | cfv 6544 |
. . . . 5
class
(.rβndx) |
8 | 4, 6 | cfv 6544 |
. . . . . 6
class
(.rβπ) |
9 | 8 | ctpos 8210 |
. . . . 5
class tpos
(.rβπ) |
10 | 7, 9 | cop 4635 |
. . . 4
class
β¨(.rβndx), tpos (.rβπ)β© |
11 | | csts 17096 |
. . . 4
class
sSet |
12 | 4, 10, 11 | co 7409 |
. . 3
class (π sSet
β¨(.rβndx), tpos (.rβπ)β©) |
13 | 2, 3, 12 | cmpt 5232 |
. 2
class (π β V β¦ (π sSet
β¨(.rβndx), tpos (.rβπ)β©)) |
14 | 1, 13 | wceq 1542 |
1
wff
oppr = (π β V β¦ (π sSet β¨(.rβndx), tpos
(.rβπ)β©)) |