Step | Hyp | Ref
| Expression |
1 | | csetc 17966 |
. 2
class
SetCat |
2 | | vu |
. . 3
setvar π’ |
3 | | cvv 3444 |
. . 3
class
V |
4 | | cnx 17070 |
. . . . . 6
class
ndx |
5 | | cbs 17088 |
. . . . . 6
class
Base |
6 | 4, 5 | cfv 6497 |
. . . . 5
class
(Baseβndx) |
7 | 2 | cv 1541 |
. . . . 5
class π’ |
8 | 6, 7 | cop 4593 |
. . . 4
class
β¨(Baseβndx), π’β© |
9 | | chom 17149 |
. . . . . 6
class
Hom |
10 | 4, 9 | cfv 6497 |
. . . . 5
class (Hom
βndx) |
11 | | vx |
. . . . . 6
setvar π₯ |
12 | | vy |
. . . . . 6
setvar π¦ |
13 | 12 | cv 1541 |
. . . . . . 7
class π¦ |
14 | 11 | cv 1541 |
. . . . . . 7
class π₯ |
15 | | cmap 8768 |
. . . . . . 7
class
βm |
16 | 13, 14, 15 | co 7358 |
. . . . . 6
class (π¦ βm π₯) |
17 | 11, 12, 7, 7, 16 | cmpo 7360 |
. . . . 5
class (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯)) |
18 | 10, 17 | cop 4593 |
. . . 4
class
β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β© |
19 | | cco 17150 |
. . . . . 6
class
comp |
20 | 4, 19 | cfv 6497 |
. . . . 5
class
(compβndx) |
21 | | vv |
. . . . . 6
setvar π£ |
22 | | vz |
. . . . . 6
setvar π§ |
23 | 7, 7 | cxp 5632 |
. . . . . 6
class (π’ Γ π’) |
24 | | vg |
. . . . . . 7
setvar π |
25 | | vf |
. . . . . . 7
setvar π |
26 | 22 | cv 1541 |
. . . . . . . 8
class π§ |
27 | 21 | cv 1541 |
. . . . . . . . 9
class π£ |
28 | | c2nd 7921 |
. . . . . . . . 9
class
2nd |
29 | 27, 28 | cfv 6497 |
. . . . . . . 8
class
(2nd βπ£) |
30 | 26, 29, 15 | co 7358 |
. . . . . . 7
class (π§ βm
(2nd βπ£)) |
31 | | c1st 7920 |
. . . . . . . . 9
class
1st |
32 | 27, 31 | cfv 6497 |
. . . . . . . 8
class
(1st βπ£) |
33 | 29, 32, 15 | co 7358 |
. . . . . . 7
class
((2nd βπ£) βm (1st
βπ£)) |
34 | 24 | cv 1541 |
. . . . . . . 8
class π |
35 | 25 | cv 1541 |
. . . . . . . 8
class π |
36 | 34, 35 | ccom 5638 |
. . . . . . 7
class (π β π) |
37 | 24, 25, 30, 33, 36 | cmpo 7360 |
. . . . . 6
class (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)) |
38 | 21, 22, 23, 7, 37 | cmpo 7360 |
. . . . 5
class (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π))) |
39 | 20, 38 | cop 4593 |
. . . 4
class
β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β© |
40 | 8, 18, 39 | ctp 4591 |
. . 3
class
{β¨(Baseβndx), π’β©, β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β©, β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β©} |
41 | 2, 3, 40 | cmpt 5189 |
. 2
class (π’ β V β¦
{β¨(Baseβndx), π’β©, β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β©, β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β©}) |
42 | 1, 41 | wceq 1542 |
1
wff SetCat =
(π’ β V β¦
{β¨(Baseβndx), π’β©, β¨(Hom βndx), (π₯ β π’, π¦ β π’ β¦ (π¦ βm π₯))β©, β¨(compβndx), (π£ β (π’ Γ π’), π§ β π’ β¦ (π β (π§ βm (2nd
βπ£)), π β ((2nd
βπ£)
βm (1st βπ£)) β¦ (π β π)))β©}) |