Step | Hyp | Ref
| Expression |
1 | | cxpc 18061 |
. 2
class
Γc |
2 | | vr |
. . 3
setvar π |
3 | | vs |
. . 3
setvar π |
4 | | cvv 3444 |
. . 3
class
V |
5 | | vb |
. . . 4
setvar π |
6 | 2 | cv 1541 |
. . . . . 6
class π |
7 | | cbs 17088 |
. . . . . 6
class
Base |
8 | 6, 7 | cfv 6497 |
. . . . 5
class
(Baseβπ) |
9 | 3 | cv 1541 |
. . . . . 6
class π |
10 | 9, 7 | cfv 6497 |
. . . . 5
class
(Baseβπ ) |
11 | 8, 10 | cxp 5632 |
. . . 4
class
((Baseβπ)
Γ (Baseβπ )) |
12 | | vh |
. . . . 5
setvar β |
13 | | vu |
. . . . . 6
setvar π’ |
14 | | vv |
. . . . . 6
setvar π£ |
15 | 5 | cv 1541 |
. . . . . 6
class π |
16 | 13 | cv 1541 |
. . . . . . . . 9
class π’ |
17 | | c1st 7920 |
. . . . . . . . 9
class
1st |
18 | 16, 17 | cfv 6497 |
. . . . . . . 8
class
(1st βπ’) |
19 | 14 | cv 1541 |
. . . . . . . . 9
class π£ |
20 | 19, 17 | cfv 6497 |
. . . . . . . 8
class
(1st βπ£) |
21 | | chom 17149 |
. . . . . . . . 9
class
Hom |
22 | 6, 21 | cfv 6497 |
. . . . . . . 8
class (Hom
βπ) |
23 | 18, 20, 22 | co 7358 |
. . . . . . 7
class
((1st βπ’)(Hom βπ)(1st βπ£)) |
24 | | c2nd 7921 |
. . . . . . . . 9
class
2nd |
25 | 16, 24 | cfv 6497 |
. . . . . . . 8
class
(2nd βπ’) |
26 | 19, 24 | cfv 6497 |
. . . . . . . 8
class
(2nd βπ£) |
27 | 9, 21 | cfv 6497 |
. . . . . . . 8
class (Hom
βπ ) |
28 | 25, 26, 27 | co 7358 |
. . . . . . 7
class
((2nd βπ’)(Hom βπ )(2nd βπ£)) |
29 | 23, 28 | cxp 5632 |
. . . . . 6
class
(((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£))) |
30 | 13, 14, 15, 15, 29 | cmpo 7360 |
. . . . 5
class (π’ β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) |
31 | | cnx 17070 |
. . . . . . . 8
class
ndx |
32 | 31, 7 | cfv 6497 |
. . . . . . 7
class
(Baseβndx) |
33 | 32, 15 | cop 4593 |
. . . . . 6
class
β¨(Baseβndx), πβ© |
34 | 31, 21 | cfv 6497 |
. . . . . . 7
class (Hom
βndx) |
35 | 12 | cv 1541 |
. . . . . . 7
class β |
36 | 34, 35 | cop 4593 |
. . . . . 6
class
β¨(Hom βndx), ββ© |
37 | | cco 17150 |
. . . . . . . 8
class
comp |
38 | 31, 37 | cfv 6497 |
. . . . . . 7
class
(compβndx) |
39 | | vx |
. . . . . . . 8
setvar π₯ |
40 | | vy |
. . . . . . . 8
setvar π¦ |
41 | 15, 15 | cxp 5632 |
. . . . . . . 8
class (π Γ π) |
42 | | vg |
. . . . . . . . 9
setvar π |
43 | | vf |
. . . . . . . . 9
setvar π |
44 | 39 | cv 1541 |
. . . . . . . . . . 11
class π₯ |
45 | 44, 24 | cfv 6497 |
. . . . . . . . . 10
class
(2nd βπ₯) |
46 | 40 | cv 1541 |
. . . . . . . . . 10
class π¦ |
47 | 45, 46, 35 | co 7358 |
. . . . . . . . 9
class
((2nd βπ₯)βπ¦) |
48 | 44, 35 | cfv 6497 |
. . . . . . . . 9
class (ββπ₯) |
49 | 42 | cv 1541 |
. . . . . . . . . . . 12
class π |
50 | 49, 17 | cfv 6497 |
. . . . . . . . . . 11
class
(1st βπ) |
51 | 43 | cv 1541 |
. . . . . . . . . . . 12
class π |
52 | 51, 17 | cfv 6497 |
. . . . . . . . . . 11
class
(1st βπ) |
53 | 44, 17 | cfv 6497 |
. . . . . . . . . . . . . 14
class
(1st βπ₯) |
54 | 53, 17 | cfv 6497 |
. . . . . . . . . . . . 13
class
(1st β(1st βπ₯)) |
55 | 45, 17 | cfv 6497 |
. . . . . . . . . . . . 13
class
(1st β(2nd βπ₯)) |
56 | 54, 55 | cop 4593 |
. . . . . . . . . . . 12
class
β¨(1st β(1st βπ₯)), (1st β(2nd
βπ₯))β© |
57 | 46, 17 | cfv 6497 |
. . . . . . . . . . . 12
class
(1st βπ¦) |
58 | 6, 37 | cfv 6497 |
. . . . . . . . . . . 12
class
(compβπ) |
59 | 56, 57, 58 | co 7358 |
. . . . . . . . . . 11
class
(β¨(1st β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦)) |
60 | 50, 52, 59 | co 7358 |
. . . . . . . . . 10
class
((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)) |
61 | 49, 24 | cfv 6497 |
. . . . . . . . . . 11
class
(2nd βπ) |
62 | 51, 24 | cfv 6497 |
. . . . . . . . . . 11
class
(2nd βπ) |
63 | 53, 24 | cfv 6497 |
. . . . . . . . . . . . 13
class
(2nd β(1st βπ₯)) |
64 | 45, 24 | cfv 6497 |
. . . . . . . . . . . . 13
class
(2nd β(2nd βπ₯)) |
65 | 63, 64 | cop 4593 |
. . . . . . . . . . . 12
class
β¨(2nd β(1st βπ₯)), (2nd β(2nd
βπ₯))β© |
66 | 46, 24 | cfv 6497 |
. . . . . . . . . . . 12
class
(2nd βπ¦) |
67 | 9, 37 | cfv 6497 |
. . . . . . . . . . . 12
class
(compβπ ) |
68 | 65, 66, 67 | co 7358 |
. . . . . . . . . . 11
class
(β¨(2nd β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦)) |
69 | 61, 62, 68 | co 7358 |
. . . . . . . . . 10
class
((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ)) |
70 | 60, 69 | cop 4593 |
. . . . . . . . 9
class
β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β© |
71 | 42, 43, 47, 48, 70 | cmpo 7360 |
. . . . . . . 8
class (π β ((2nd
βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©) |
72 | 39, 40, 41, 15, 71 | cmpo 7360 |
. . . . . . 7
class (π₯ β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©)) |
73 | 38, 72 | cop 4593 |
. . . . . 6
class
β¨(compβndx), (π₯ β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β© |
74 | 33, 36, 73 | ctp 4591 |
. . . . 5
class
{β¨(Baseβndx), πβ©, β¨(Hom βndx), ββ©, β¨(compβndx),
(π₯ β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©} |
75 | 12, 30, 74 | csb 3856 |
. . . 4
class
β¦(π’
β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) / ββ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
ββ©,
β¨(compβndx), (π₯
β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©} |
76 | 5, 11, 75 | csb 3856 |
. . 3
class
β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¦(π’ β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) / ββ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
ββ©,
β¨(compβndx), (π₯
β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©} |
77 | 2, 3, 4, 4, 76 | cmpo 7360 |
. 2
class (π β V, π β V β¦
β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¦(π’ β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) / ββ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
ββ©,
β¨(compβndx), (π₯
β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©}) |
78 | 1, 77 | wceq 1542 |
1
wff
Γc = (π β V, π β V β¦
β¦((Baseβπ) Γ (Baseβπ )) / πβ¦β¦(π’ β π, π£ β π β¦ (((1st βπ’)(Hom βπ)(1st βπ£)) Γ ((2nd βπ’)(Hom βπ )(2nd βπ£)))) / ββ¦{β¨(Baseβndx), πβ©, β¨(Hom βndx),
ββ©,
β¨(compβndx), (π₯
β (π Γ π), π¦ β π β¦ (π β ((2nd βπ₯)βπ¦), π β (ββπ₯) β¦ β¨((1st βπ)(β¨(1st
β(1st βπ₯)), (1st β(2nd
βπ₯))β©(compβπ)(1st βπ¦))(1st βπ)), ((2nd βπ)(β¨(2nd
β(1st βπ₯)), (2nd β(2nd
βπ₯))β©(compβπ )(2nd βπ¦))(2nd βπ))β©))β©}) |