Step | Hyp | Ref
| Expression |
1 | | cresc 17754 |
. 2
class
βΎcat |
2 | | vc |
. . 3
setvar π |
3 | | vh |
. . 3
setvar β |
4 | | cvv 3474 |
. . 3
class
V |
5 | 2 | cv 1540 |
. . . . 5
class π |
6 | 3 | cv 1540 |
. . . . . . 7
class β |
7 | 6 | cdm 5676 |
. . . . . 6
class dom β |
8 | 7 | cdm 5676 |
. . . . 5
class dom dom
β |
9 | | cress 17172 |
. . . . 5
class
βΎs |
10 | 5, 8, 9 | co 7408 |
. . . 4
class (π βΎs dom dom
β) |
11 | | cnx 17125 |
. . . . . 6
class
ndx |
12 | | chom 17207 |
. . . . . 6
class
Hom |
13 | 11, 12 | cfv 6543 |
. . . . 5
class (Hom
βndx) |
14 | 13, 6 | cop 4634 |
. . . 4
class
β¨(Hom βndx), ββ© |
15 | | csts 17095 |
. . . 4
class
sSet |
16 | 10, 14, 15 | co 7408 |
. . 3
class ((π βΎs dom dom
β) sSet β¨(Hom
βndx), ββ©) |
17 | 2, 3, 4, 4, 16 | cmpo 7410 |
. 2
class (π β V, β β V β¦ ((π βΎs dom dom β) sSet β¨(Hom βndx),
ββ©)) |
18 | 1, 17 | wceq 1541 |
1
wff
βΎcat = (π
β V, β β V β¦
((π βΎs dom
dom β) sSet β¨(Hom
βndx), ββ©)) |