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