Step | Hyp | Ref
| Expression |
1 | | sectmon.1 |
. . . 4
β’ (π β πΉ(πππ)πΊ) |
2 | | sectmon.b |
. . . . 5
β’ π΅ = (BaseβπΆ) |
3 | | eqid 2733 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
4 | | eqid 2733 |
. . . . 5
β’
(compβπΆ) =
(compβπΆ) |
5 | | eqid 2733 |
. . . . 5
β’
(IdβπΆ) =
(IdβπΆ) |
6 | | sectmon.s |
. . . . 5
β’ π = (SectβπΆ) |
7 | | sectmon.c |
. . . . 5
β’ (π β πΆ β Cat) |
8 | | sectmon.x |
. . . . 5
β’ (π β π β π΅) |
9 | | sectmon.y |
. . . . 5
β’ (π β π β π΅) |
10 | 2, 3, 4, 5, 6, 7, 8, 9 | issect 17700 |
. . . 4
β’ (π β (πΉ(πππ)πΊ β (πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)))) |
11 | 1, 10 | mpbid 231 |
. . 3
β’ (π β (πΉ β (π(Hom βπΆ)π) β§ πΊ β (π(Hom βπΆ)π) β§ (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ))) |
12 | 11 | simp1d 1143 |
. 2
β’ (π β πΉ β (π(Hom βπΆ)π)) |
13 | | oveq2 7417 |
. . . . 5
β’ ((πΉ(β¨π₯, πβ©(compβπΆ)π)π) = (πΉ(β¨π₯, πβ©(compβπΆ)π)β) β (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)π)) = (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)β))) |
14 | 11 | simp3d 1145 |
. . . . . . . . 9
β’ (π β (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) |
15 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β (πΊ(β¨π, πβ©(compβπΆ)π)πΉ) = ((IdβπΆ)βπ)) |
16 | 15 | oveq1d 7424 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ)(β¨π₯, πβ©(compβπΆ)π)π) = (((IdβπΆ)βπ)(β¨π₯, πβ©(compβπΆ)π)π)) |
17 | 7 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β πΆ β Cat) |
18 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β π₯ β π΅) |
19 | 8 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β π β π΅) |
20 | 9 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β π β π΅) |
21 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β π β (π₯(Hom βπΆ)π)) |
22 | 12 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β πΉ β (π(Hom βπΆ)π)) |
23 | 11 | simp2d 1144 |
. . . . . . . . 9
β’ (π β πΊ β (π(Hom βπΆ)π)) |
24 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β πΊ β (π(Hom βπΆ)π)) |
25 | 2, 3, 4, 17, 18, 19, 20, 21, 22, 19, 24 | catass 17630 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ)(β¨π₯, πβ©(compβπΆ)π)π) = (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)π))) |
26 | 2, 3, 5, 17, 18, 4, 19, 21 | catlid 17627 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β (((IdβπΆ)βπ)(β¨π₯, πβ©(compβπΆ)π)π) = π) |
27 | 16, 25, 26 | 3eqtr3d 2781 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)π)) = π) |
28 | 15 | oveq1d 7424 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ)(β¨π₯, πβ©(compβπΆ)π)β) = (((IdβπΆ)βπ)(β¨π₯, πβ©(compβπΆ)π)β)) |
29 | | simprr 772 |
. . . . . . . 8
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β β β (π₯(Hom βπΆ)π)) |
30 | 2, 3, 4, 17, 18, 19, 20, 29, 22, 19, 24 | catass 17630 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β ((πΊ(β¨π, πβ©(compβπΆ)π)πΉ)(β¨π₯, πβ©(compβπΆ)π)β) = (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)β))) |
31 | 2, 3, 5, 17, 18, 4, 19, 29 | catlid 17627 |
. . . . . . 7
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β (((IdβπΆ)βπ)(β¨π₯, πβ©(compβπΆ)π)β) = β) |
32 | 28, 30, 31 | 3eqtr3d 2781 |
. . . . . 6
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)β)) = β) |
33 | 27, 32 | eqeq12d 2749 |
. . . . 5
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β ((πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)π)) = (πΊ(β¨π₯, πβ©(compβπΆ)π)(πΉ(β¨π₯, πβ©(compβπΆ)π)β)) β π = β)) |
34 | 13, 33 | imbitrid 243 |
. . . 4
β’ (((π β§ π₯ β π΅) β§ (π β (π₯(Hom βπΆ)π) β§ β β (π₯(Hom βπΆ)π))) β ((πΉ(β¨π₯, πβ©(compβπΆ)π)π) = (πΉ(β¨π₯, πβ©(compβπΆ)π)β) β π = β)) |
35 | 34 | ralrimivva 3201 |
. . 3
β’ ((π β§ π₯ β π΅) β βπ β (π₯(Hom βπΆ)π)ββ β (π₯(Hom βπΆ)π)((πΉ(β¨π₯, πβ©(compβπΆ)π)π) = (πΉ(β¨π₯, πβ©(compβπΆ)π)β) β π = β)) |
36 | 35 | ralrimiva 3147 |
. 2
β’ (π β βπ₯ β π΅ βπ β (π₯(Hom βπΆ)π)ββ β (π₯(Hom βπΆ)π)((πΉ(β¨π₯, πβ©(compβπΆ)π)π) = (πΉ(β¨π₯, πβ©(compβπΆ)π)β) β π = β)) |
37 | | sectmon.m |
. . 3
β’ π = (MonoβπΆ) |
38 | 2, 3, 4, 37, 7, 8,
9 | ismon2 17681 |
. 2
β’ (π β (πΉ β (πππ) β (πΉ β (π(Hom βπΆ)π) β§ βπ₯ β π΅ βπ β (π₯(Hom βπΆ)π)ββ β (π₯(Hom βπΆ)π)((πΉ(β¨π₯, πβ©(compβπΆ)π)π) = (πΉ(β¨π₯, πβ©(compβπΆ)π)β) β π = β)))) |
39 | 12, 36, 38 | mpbir2and 712 |
1
β’ (π β πΉ β (πππ)) |