Step | Hyp | Ref
| Expression |
1 | | setccat.c |
. . 3
β’ πΆ = (SetCatβπ) |
2 | | id 22 |
. . 3
β’ (π β π β π β π) |
3 | 1, 2 | setcbas 17969 |
. 2
β’ (π β π β π = (BaseβπΆ)) |
4 | | eqidd 2734 |
. 2
β’ (π β π β (Hom βπΆ) = (Hom βπΆ)) |
5 | | eqidd 2734 |
. 2
β’ (π β π β (compβπΆ) = (compβπΆ)) |
6 | 1 | fvexi 6857 |
. . 3
β’ πΆ β V |
7 | 6 | a1i 11 |
. 2
β’ (π β π β πΆ β V) |
8 | | biid 261 |
. 2
β’ (((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§))) β ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) |
9 | | f1oi 6823 |
. . . 4
β’ ( I
βΎ π₯):π₯β1-1-ontoβπ₯ |
10 | | f1of 6785 |
. . . 4
β’ (( I
βΎ π₯):π₯β1-1-ontoβπ₯ β ( I βΎ π₯):π₯βΆπ₯) |
11 | 9, 10 | mp1i 13 |
. . 3
β’ ((π β π β§ π₯ β π) β ( I βΎ π₯):π₯βΆπ₯) |
12 | | simpl 484 |
. . . 4
β’ ((π β π β§ π₯ β π) β π β π) |
13 | | eqid 2733 |
. . . 4
β’ (Hom
βπΆ) = (Hom
βπΆ) |
14 | | simpr 486 |
. . . 4
β’ ((π β π β§ π₯ β π) β π₯ β π) |
15 | 1, 12, 13, 14, 14 | elsetchom 17972 |
. . 3
β’ ((π β π β§ π₯ β π) β (( I βΎ π₯) β (π₯(Hom βπΆ)π₯) β ( I βΎ π₯):π₯βΆπ₯)) |
16 | 11, 15 | mpbird 257 |
. 2
β’ ((π β π β§ π₯ β π) β ( I βΎ π₯) β (π₯(Hom βπΆ)π₯)) |
17 | | simpl 484 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π β π) |
18 | | eqid 2733 |
. . . 4
β’
(compβπΆ) =
(compβπΆ) |
19 | | simpr1l 1231 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π€ β π) |
20 | | simpr1r 1232 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π₯ β π) |
21 | | simpr31 1264 |
. . . . 5
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π β (π€(Hom βπΆ)π₯)) |
22 | 1, 17, 13, 19, 20 | elsetchom 17972 |
. . . . 5
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π β (π€(Hom βπΆ)π₯) β π:π€βΆπ₯)) |
23 | 21, 22 | mpbid 231 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π:π€βΆπ₯) |
24 | 9, 10 | mp1i 13 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β ( I βΎ π₯):π₯βΆπ₯) |
25 | 1, 17, 18, 19, 20, 20, 23, 24 | setcco 17974 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (( I βΎ π₯)(β¨π€, π₯β©(compβπΆ)π₯)π) = (( I βΎ π₯) β π)) |
26 | | fcoi2 6718 |
. . . 4
β’ (π:π€βΆπ₯ β (( I βΎ π₯) β π) = π) |
27 | 23, 26 | syl 17 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (( I βΎ π₯) β π) = π) |
28 | 25, 27 | eqtrd 2773 |
. 2
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (( I βΎ π₯)(β¨π€, π₯β©(compβπΆ)π₯)π) = π) |
29 | | simpr2l 1233 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π¦ β π) |
30 | | simpr32 1265 |
. . . . 5
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π β (π₯(Hom βπΆ)π¦)) |
31 | 1, 17, 13, 20, 29 | elsetchom 17972 |
. . . . 5
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π β (π₯(Hom βπΆ)π¦) β π:π₯βΆπ¦)) |
32 | 30, 31 | mpbid 231 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π:π₯βΆπ¦) |
33 | 1, 17, 18, 20, 20, 29, 24, 32 | setcco 17974 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π(β¨π₯, π₯β©(compβπΆ)π¦)( I βΎ π₯)) = (π β ( I βΎ π₯))) |
34 | | fcoi1 6717 |
. . . 4
β’ (π:π₯βΆπ¦ β (π β ( I βΎ π₯)) = π) |
35 | 32, 34 | syl 17 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π β ( I βΎ π₯)) = π) |
36 | 33, 35 | eqtrd 2773 |
. 2
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π(β¨π₯, π₯β©(compβπΆ)π¦)( I βΎ π₯)) = π) |
37 | 1, 17, 18, 19, 20, 29, 23, 32 | setcco 17974 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π(β¨π€, π₯β©(compβπΆ)π¦)π) = (π β π)) |
38 | | fco 6693 |
. . . . 5
β’ ((π:π₯βΆπ¦ β§ π:π€βΆπ₯) β (π β π):π€βΆπ¦) |
39 | 32, 23, 38 | syl2anc 585 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π β π):π€βΆπ¦) |
40 | 1, 17, 13, 19, 29 | elsetchom 17972 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β ((π β π) β (π€(Hom βπΆ)π¦) β (π β π):π€βΆπ¦)) |
41 | 39, 40 | mpbird 257 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π β π) β (π€(Hom βπΆ)π¦)) |
42 | 37, 41 | eqeltrd 2834 |
. 2
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (π(β¨π€, π₯β©(compβπΆ)π¦)π) β (π€(Hom βπΆ)π¦)) |
43 | | coass 6218 |
. . . 4
β’ ((β β π) β π) = (β β (π β π)) |
44 | | simpr2r 1234 |
. . . . 5
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β π§ β π) |
45 | | simpr33 1266 |
. . . . . . 7
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β β β (π¦(Hom βπΆ)π§)) |
46 | 1, 17, 13, 29, 44 | elsetchom 17972 |
. . . . . . 7
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (β β (π¦(Hom βπΆ)π§) β β:π¦βΆπ§)) |
47 | 45, 46 | mpbid 231 |
. . . . . 6
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β β:π¦βΆπ§) |
48 | | fco 6693 |
. . . . . 6
β’ ((β:π¦βΆπ§ β§ π:π₯βΆπ¦) β (β β π):π₯βΆπ§) |
49 | 47, 32, 48 | syl2anc 585 |
. . . . 5
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (β β π):π₯βΆπ§) |
50 | 1, 17, 18, 19, 20, 44, 23, 49 | setcco 17974 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β ((β β π)(β¨π€, π₯β©(compβπΆ)π§)π) = ((β β π) β π)) |
51 | 1, 17, 18, 19, 29, 44, 39, 47 | setcco 17974 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (β(β¨π€, π¦β©(compβπΆ)π§)(π β π)) = (β β (π β π))) |
52 | 43, 50, 51 | 3eqtr4a 2799 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β ((β β π)(β¨π€, π₯β©(compβπΆ)π§)π) = (β(β¨π€, π¦β©(compβπΆ)π§)(π β π))) |
53 | 1, 17, 18, 20, 29, 44, 32, 47 | setcco 17974 |
. . . 4
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (β(β¨π₯, π¦β©(compβπΆ)π§)π) = (β β π)) |
54 | 53 | oveq1d 7373 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β ((β(β¨π₯, π¦β©(compβπΆ)π§)π)(β¨π€, π₯β©(compβπΆ)π§)π) = ((β β π)(β¨π€, π₯β©(compβπΆ)π§)π)) |
55 | 37 | oveq2d 7374 |
. . 3
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β (β(β¨π€, π¦β©(compβπΆ)π§)(π(β¨π€, π₯β©(compβπΆ)π¦)π)) = (β(β¨π€, π¦β©(compβπΆ)π§)(π β π))) |
56 | 52, 54, 55 | 3eqtr4d 2783 |
. 2
β’ ((π β π β§ ((π€ β π β§ π₯ β π) β§ (π¦ β π β§ π§ β π) β§ (π β (π€(Hom βπΆ)π₯) β§ π β (π₯(Hom βπΆ)π¦) β§ β β (π¦(Hom βπΆ)π§)))) β ((β(β¨π₯, π¦β©(compβπΆ)π§)π)(β¨π€, π₯β©(compβπΆ)π§)π) = (β(β¨π€, π¦β©(compβπΆ)π§)(π(β¨π€, π₯β©(compβπΆ)π¦)π))) |
57 | 3, 4, 5, 7, 8, 16,
28, 36, 42, 56 | iscatd2 17566 |
1
β’ (π β π β (πΆ β Cat β§ (IdβπΆ) = (π₯ β π β¦ ( I βΎ π₯)))) |