Step | Hyp | Ref
| Expression |
1 | | ismon.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | ismon.h |
. . 3
β’ π» = (Hom βπΆ) |
3 | | ismon.o |
. . 3
β’ Β· =
(compβπΆ) |
4 | | ismon.s |
. . 3
β’ π = (MonoβπΆ) |
5 | | ismon.c |
. . 3
β’ (π β πΆ β Cat) |
6 | | ismon.x |
. . 3
β’ (π β π β π΅) |
7 | | ismon.y |
. . 3
β’ (π β π β π΅) |
8 | 1, 2, 3, 4, 5, 6, 7 | ismon 17676 |
. 2
β’ (π β (πΉ β (πππ) β (πΉ β (ππ»π) β§ βπ§ β π΅ Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π))))) |
9 | 5 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β πΆ β Cat) |
10 | | simprl 769 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β π§ β π΅) |
11 | 6 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β π β π΅) |
12 | 7 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β π β π΅) |
13 | | simprr 771 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β π β (π§π»π)) |
14 | | simplr 767 |
. . . . . . . 8
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β πΉ β (ππ»π)) |
15 | 1, 2, 3, 9, 10, 11, 12, 13, 14 | catcocl 17625 |
. . . . . . 7
β’ (((π β§ πΉ β (ππ»π)) β§ (π§ β π΅ β§ π β (π§π»π))) β (πΉ(β¨π§, πβ© Β· π)π) β (π§π»π)) |
16 | 15 | anassrs 468 |
. . . . . 6
β’ ((((π β§ πΉ β (ππ»π)) β§ π§ β π΅) β§ π β (π§π»π)) β (πΉ(β¨π§, πβ© Β· π)π) β (π§π»π)) |
17 | 16 | ralrimiva 3146 |
. . . . 5
β’ (((π β§ πΉ β (ππ»π)) β§ π§ β π΅) β βπ β (π§π»π)(πΉ(β¨π§, πβ© Β· π)π) β (π§π»π)) |
18 | | eqid 2732 |
. . . . . . . 8
β’ (π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)) = (π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)) |
19 | 18 | fmpt 7106 |
. . . . . . 7
β’
(βπ β
(π§π»π)(πΉ(β¨π§, πβ© Β· π)π) β (π§π»π) β (π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)βΆ(π§π»π)) |
20 | | df-f1 6545 |
. . . . . . . 8
β’ ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)β1-1β(π§π»π) β ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)βΆ(π§π»π) β§ Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)))) |
21 | 20 | baib 536 |
. . . . . . 7
β’ ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)βΆ(π§π»π) β ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)β1-1β(π§π»π) β Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)))) |
22 | 19, 21 | sylbi 216 |
. . . . . 6
β’
(βπ β
(π§π»π)(πΉ(β¨π§, πβ© Β· π)π) β (π§π»π) β ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)β1-1β(π§π»π) β Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)))) |
23 | | oveq2 7413 |
. . . . . . . 8
β’ (π = β β (πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β)) |
24 | 18, 23 | f1mpt 7256 |
. . . . . . 7
β’ ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)β1-1β(π§π»π) β (βπ β (π§π»π)(πΉ(β¨π§, πβ© Β· π)π) β (π§π»π) β§ βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β))) |
25 | 24 | baib 536 |
. . . . . 6
β’
(βπ β
(π§π»π)(πΉ(β¨π§, πβ© Β· π)π) β (π§π»π) β ((π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)):(π§π»π)β1-1β(π§π»π) β βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β))) |
26 | 22, 25 | bitr3d 280 |
. . . . 5
β’
(βπ β
(π§π»π)(πΉ(β¨π§, πβ© Β· π)π) β (π§π»π) β (Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)) β βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β))) |
27 | 17, 26 | syl 17 |
. . . 4
β’ (((π β§ πΉ β (ππ»π)) β§ π§ β π΅) β (Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)) β βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β))) |
28 | 27 | ralbidva 3175 |
. . 3
β’ ((π β§ πΉ β (ππ»π)) β (βπ§ β π΅ Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π)) β βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β))) |
29 | 28 | pm5.32da 579 |
. 2
β’ (π β ((πΉ β (ππ»π) β§ βπ§ β π΅ Fun β‘(π β (π§π»π) β¦ (πΉ(β¨π§, πβ© Β· π)π))) β (πΉ β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β)))) |
30 | 8, 29 | bitrd 278 |
1
β’ (π β (πΉ β (πππ) β (πΉ β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)ββ β (π§π»π)((πΉ(β¨π§, πβ© Β· π)π) = (πΉ(β¨π§, πβ© Β· π)β) β π = β)))) |