Step | Hyp | Ref
| Expression |
1 | | oppcbas.1 |
. . . . 5
β’ π = (oppCatβπΆ) |
2 | | eqid 2733 |
. . . . 5
β’
(BaseβπΆ) =
(BaseβπΆ) |
3 | 1, 2 | oppcbas 17607 |
. . . 4
β’
(BaseβπΆ) =
(Baseβπ) |
4 | 3 | a1i 11 |
. . 3
β’ (πΆ β Cat β
(BaseβπΆ) =
(Baseβπ)) |
5 | | eqidd 2734 |
. . 3
β’ (πΆ β Cat β (Hom
βπ) = (Hom
βπ)) |
6 | | eqidd 2734 |
. . 3
β’ (πΆ β Cat β
(compβπ) =
(compβπ)) |
7 | 1 | fvexi 6860 |
. . . 4
β’ π β V |
8 | 7 | a1i 11 |
. . 3
β’ (πΆ β Cat β π β V) |
9 | | biid 261 |
. . 3
β’ (((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€))) β ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) |
10 | | eqid 2733 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
11 | | eqid 2733 |
. . . . 5
β’
(IdβπΆ) =
(IdβπΆ) |
12 | | simpl 484 |
. . . . 5
β’ ((πΆ β Cat β§ π¦ β (BaseβπΆ)) β πΆ β Cat) |
13 | | simpr 486 |
. . . . 5
β’ ((πΆ β Cat β§ π¦ β (BaseβπΆ)) β π¦ β (BaseβπΆ)) |
14 | 2, 10, 11, 12, 13 | catidcl 17570 |
. . . 4
β’ ((πΆ β Cat β§ π¦ β (BaseβπΆ)) β ((IdβπΆ)βπ¦) β (π¦(Hom βπΆ)π¦)) |
15 | 10, 1 | oppchom 17604 |
. . . 4
β’ (π¦(Hom βπ)π¦) = (π¦(Hom βπΆ)π¦) |
16 | 14, 15 | eleqtrrdi 2845 |
. . 3
β’ ((πΆ β Cat β§ π¦ β (BaseβπΆ)) β ((IdβπΆ)βπ¦) β (π¦(Hom βπ)π¦)) |
17 | | eqid 2733 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
18 | | simpr1l 1231 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π₯ β (BaseβπΆ)) |
19 | | simpr1r 1232 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π¦ β (BaseβπΆ)) |
20 | 2, 17, 1, 18, 19, 19 | oppcco 17606 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (((IdβπΆ)βπ¦)(β¨π₯, π¦β©(compβπ)π¦)π) = (π(β¨π¦, π¦β©(compβπΆ)π₯)((IdβπΆ)βπ¦))) |
21 | | simpl 484 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β πΆ β Cat) |
22 | | simpr31 1264 |
. . . . . 6
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π β (π₯(Hom βπ)π¦)) |
23 | 10, 1 | oppchom 17604 |
. . . . . 6
β’ (π₯(Hom βπ)π¦) = (π¦(Hom βπΆ)π₯) |
24 | 22, 23 | eleqtrdi 2844 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π β (π¦(Hom βπΆ)π₯)) |
25 | 2, 10, 11, 21, 19, 17, 18, 24 | catrid 17572 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π¦, π¦β©(compβπΆ)π₯)((IdβπΆ)βπ¦)) = π) |
26 | 20, 25 | eqtrd 2773 |
. . 3
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (((IdβπΆ)βπ¦)(β¨π₯, π¦β©(compβπ)π¦)π) = π) |
27 | | simpr2l 1233 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π§ β (BaseβπΆ)) |
28 | 2, 17, 1, 19, 19, 27 | oppcco 17606 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π¦, π¦β©(compβπ)π§)((IdβπΆ)βπ¦)) = (((IdβπΆ)βπ¦)(β¨π§, π¦β©(compβπΆ)π¦)π)) |
29 | | simpr32 1265 |
. . . . . 6
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π β (π¦(Hom βπ)π§)) |
30 | 10, 1 | oppchom 17604 |
. . . . . 6
β’ (π¦(Hom βπ)π§) = (π§(Hom βπΆ)π¦) |
31 | 29, 30 | eleqtrdi 2844 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π β (π§(Hom βπΆ)π¦)) |
32 | 2, 10, 11, 21, 27, 17, 19, 31 | catlid 17571 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (((IdβπΆ)βπ¦)(β¨π§, π¦β©(compβπΆ)π¦)π) = π) |
33 | 28, 32 | eqtrd 2773 |
. . 3
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π¦, π¦β©(compβπ)π§)((IdβπΆ)βπ¦)) = π) |
34 | 2, 17, 1, 18, 19, 27 | oppcco 17606 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π₯, π¦β©(compβπ)π§)π) = (π(β¨π§, π¦β©(compβπΆ)π₯)π)) |
35 | 2, 10, 17, 21, 27, 19, 18, 31, 24 | catcocl 17573 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π§, π¦β©(compβπΆ)π₯)π) β (π§(Hom βπΆ)π₯)) |
36 | 34, 35 | eqeltrd 2834 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π₯, π¦β©(compβπ)π§)π) β (π§(Hom βπΆ)π₯)) |
37 | 10, 1 | oppchom 17604 |
. . . 4
β’ (π₯(Hom βπ)π§) = (π§(Hom βπΆ)π₯) |
38 | 36, 37 | eleqtrrdi 2845 |
. . 3
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (π(β¨π₯, π¦β©(compβπ)π§)π) β (π₯(Hom βπ)π§)) |
39 | | simpr2r 1234 |
. . . . . 6
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β π€ β (BaseβπΆ)) |
40 | | simpr33 1266 |
. . . . . . 7
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β β β (π§(Hom βπ)π€)) |
41 | 10, 1 | oppchom 17604 |
. . . . . . 7
β’ (π§(Hom βπ)π€) = (π€(Hom βπΆ)π§) |
42 | 40, 41 | eleqtrdi 2844 |
. . . . . 6
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β β β (π€(Hom βπΆ)π§)) |
43 | 2, 10, 17, 21, 39, 27, 19, 42, 31, 18, 24 | catass 17574 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β ((π(β¨π§, π¦β©(compβπΆ)π₯)π)(β¨π€, π§β©(compβπΆ)π₯)β) = (π(β¨π€, π¦β©(compβπΆ)π₯)(π(β¨π€, π§β©(compβπΆ)π¦)β))) |
44 | 2, 17, 1, 18, 27, 39 | oppcco 17606 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (β(β¨π₯, π§β©(compβπ)π€)(π(β¨π§, π¦β©(compβπΆ)π₯)π)) = ((π(β¨π§, π¦β©(compβπΆ)π₯)π)(β¨π€, π§β©(compβπΆ)π₯)β)) |
45 | 2, 17, 1, 18, 19, 39 | oppcco 17606 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β ((π(β¨π€, π§β©(compβπΆ)π¦)β)(β¨π₯, π¦β©(compβπ)π€)π) = (π(β¨π€, π¦β©(compβπΆ)π₯)(π(β¨π€, π§β©(compβπΆ)π¦)β))) |
46 | 43, 44, 45 | 3eqtr4rd 2784 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β ((π(β¨π€, π§β©(compβπΆ)π¦)β)(β¨π₯, π¦β©(compβπ)π€)π) = (β(β¨π₯, π§β©(compβπ)π€)(π(β¨π§, π¦β©(compβπΆ)π₯)π))) |
47 | 2, 17, 1, 19, 27, 39 | oppcco 17606 |
. . . . 5
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (β(β¨π¦, π§β©(compβπ)π€)π) = (π(β¨π€, π§β©(compβπΆ)π¦)β)) |
48 | 47 | oveq1d 7376 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β ((β(β¨π¦, π§β©(compβπ)π€)π)(β¨π₯, π¦β©(compβπ)π€)π) = ((π(β¨π€, π§β©(compβπΆ)π¦)β)(β¨π₯, π¦β©(compβπ)π€)π)) |
49 | 34 | oveq2d 7377 |
. . . 4
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β (β(β¨π₯, π§β©(compβπ)π€)(π(β¨π₯, π¦β©(compβπ)π§)π)) = (β(β¨π₯, π§β©(compβπ)π€)(π(β¨π§, π¦β©(compβπΆ)π₯)π))) |
50 | 46, 48, 49 | 3eqtr4d 2783 |
. . 3
β’ ((πΆ β Cat β§ ((π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ)) β§ (π§ β (BaseβπΆ) β§ π€ β (BaseβπΆ)) β§ (π β (π₯(Hom βπ)π¦) β§ π β (π¦(Hom βπ)π§) β§ β β (π§(Hom βπ)π€)))) β ((β(β¨π¦, π§β©(compβπ)π€)π)(β¨π₯, π¦β©(compβπ)π€)π) = (β(β¨π₯, π§β©(compβπ)π€)(π(β¨π₯, π¦β©(compβπ)π§)π))) |
51 | 4, 5, 6, 8, 9, 16,
26, 33, 38, 50 | iscatd2 17569 |
. 2
β’ (πΆ β Cat β (π β Cat β§
(Idβπ) = (π¦ β (BaseβπΆ) β¦ ((IdβπΆ)βπ¦)))) |
52 | 2, 11 | cidfn 17567 |
. . . . 5
β’ (πΆ β Cat β
(IdβπΆ) Fn
(BaseβπΆ)) |
53 | | dffn5 6905 |
. . . . 5
β’
((IdβπΆ) Fn
(BaseβπΆ) β
(IdβπΆ) = (π¦ β (BaseβπΆ) β¦ ((IdβπΆ)βπ¦))) |
54 | 52, 53 | sylib 217 |
. . . 4
β’ (πΆ β Cat β
(IdβπΆ) = (π¦ β (BaseβπΆ) β¦ ((IdβπΆ)βπ¦))) |
55 | 54 | eqeq2d 2744 |
. . 3
β’ (πΆ β Cat β
((Idβπ) =
(IdβπΆ) β
(Idβπ) = (π¦ β (BaseβπΆ) β¦ ((IdβπΆ)βπ¦)))) |
56 | 55 | anbi2d 630 |
. 2
β’ (πΆ β Cat β ((π β Cat β§
(Idβπ) =
(IdβπΆ)) β (π β Cat β§
(Idβπ) = (π¦ β (BaseβπΆ) β¦ ((IdβπΆ)βπ¦))))) |
57 | 51, 56 | mpbird 257 |
1
β’ (πΆ β Cat β (π β Cat β§
(Idβπ) =
(IdβπΆ))) |