Step | Hyp | Ref
| Expression |
1 | | cresc 17759 |
. 2
class
βΎcat |
2 | | vc |
. . 3
setvar π |
3 | | vh |
. . 3
setvar β |
4 | | cvv 3472 |
. . 3
class
V |
5 | 2 | cv 1538 |
. . . . 5
class π |
6 | 3 | cv 1538 |
. . . . . . 7
class β |
7 | 6 | cdm 5675 |
. . . . . 6
class dom β |
8 | 7 | cdm 5675 |
. . . . 5
class dom dom
β |
9 | | cress 17177 |
. . . . 5
class
βΎs |
10 | 5, 8, 9 | co 7411 |
. . . 4
class (π βΎs dom dom
β) |
11 | | cnx 17130 |
. . . . . 6
class
ndx |
12 | | chom 17212 |
. . . . . 6
class
Hom |
13 | 11, 12 | cfv 6542 |
. . . . 5
class (Hom
βndx) |
14 | 13, 6 | cop 4633 |
. . . 4
class
β¨(Hom βndx), ββ© |
15 | | csts 17100 |
. . . 4
class
sSet |
16 | 10, 14, 15 | co 7411 |
. . 3
class ((π βΎs dom dom
β) sSet β¨(Hom
βndx), ββ©) |
17 | 2, 3, 4, 4, 16 | cmpo 7413 |
. 2
class (π β V, β β V β¦ ((π βΎs dom dom β) sSet β¨(Hom βndx),
ββ©)) |
18 | 1, 17 | wceq 1539 |
1
wff
βΎcat = (π
β V, β β V β¦
((π βΎs dom
dom β) sSet β¨(Hom
βndx), ββ©)) |