Step | Hyp | Ref
| Expression |
1 | | coppr 13237 |
. 2
class
oppr |
2 | | vf |
. . 3
setvar π |
3 | | cvv 2737 |
. . 3
class
V |
4 | 2 | cv 1352 |
. . . 4
class π |
5 | | cnx 12458 |
. . . . . 6
class
ndx |
6 | | cmulr 12536 |
. . . . . 6
class
.r |
7 | 5, 6 | cfv 5216 |
. . . . 5
class
(.rβndx) |
8 | 4, 6 | cfv 5216 |
. . . . . 6
class
(.rβπ) |
9 | 8 | ctpos 6244 |
. . . . 5
class tpos
(.rβπ) |
10 | 7, 9 | cop 3595 |
. . . 4
class
β¨(.rβndx), tpos (.rβπ)β© |
11 | | csts 12459 |
. . . 4
class
sSet |
12 | 4, 10, 11 | co 5874 |
. . 3
class (π sSet
β¨(.rβndx), tpos (.rβπ)β©) |
13 | 2, 3, 12 | cmpt 4064 |
. 2
class (π β V β¦ (π sSet
β¨(.rβndx), tpos (.rβπ)β©)) |
14 | 1, 13 | wceq 1353 |
1
wff
oppr = (π β V β¦ (π sSet β¨(.rβndx), tpos
(.rβπ)β©)) |