Step | Hyp | Ref
| Expression |
1 | | fthmon.r |
. 2
β’ (π β π
β (ππ»π)) |
2 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ·) =
(Baseβπ·) |
3 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπ·) = (Hom
βπ·) |
4 | | eqid 2733 |
. . . . . 6
β’
(compβπ·) =
(compβπ·) |
5 | | fthmon.n |
. . . . . 6
β’ π = (Monoβπ·) |
6 | | fthmon.f |
. . . . . . . . . . 11
β’ (π β πΉ(πΆ Faith π·)πΊ) |
7 | | fthfunc 17799 |
. . . . . . . . . . . 12
β’ (πΆ Faith π·) β (πΆ Func π·) |
8 | 7 | ssbri 5151 |
. . . . . . . . . . 11
β’ (πΉ(πΆ Faith π·)πΊ β πΉ(πΆ Func π·)πΊ) |
9 | 6, 8 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ(πΆ Func π·)πΊ) |
10 | | df-br 5107 |
. . . . . . . . . 10
β’ (πΉ(πΆ Func π·)πΊ β β¨πΉ, πΊβ© β (πΆ Func π·)) |
11 | 9, 10 | sylib 217 |
. . . . . . . . 9
β’ (π β β¨πΉ, πΊβ© β (πΆ Func π·)) |
12 | | funcrcl 17754 |
. . . . . . . . 9
β’
(β¨πΉ, πΊβ© β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
β’ (π β (πΆ β Cat β§ π· β Cat)) |
14 | 13 | simprd 497 |
. . . . . . 7
β’ (π β π· β Cat) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π· β Cat) |
16 | | fthmon.b |
. . . . . . . 8
β’ π΅ = (BaseβπΆ) |
17 | 9 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β πΉ(πΆ Func π·)πΊ) |
18 | 16, 2, 17 | funcf1 17757 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β πΉ:π΅βΆ(Baseβπ·)) |
19 | | fthmon.x |
. . . . . . . 8
β’ (π β π β π΅) |
20 | 19 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π β π΅) |
21 | 18, 20 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (πΉβπ) β (Baseβπ·)) |
22 | | fthmon.y |
. . . . . . . 8
β’ (π β π β π΅) |
23 | 22 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π β π΅) |
24 | 18, 23 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (πΉβπ) β (Baseβπ·)) |
25 | | simpr1 1195 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π§ β π΅) |
26 | 18, 25 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (πΉβπ§) β (Baseβπ·)) |
27 | | fthmon.1 |
. . . . . . 7
β’ (π β ((ππΊπ)βπ
) β ((πΉβπ)π(πΉβπ))) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((ππΊπ)βπ
) β ((πΉβπ)π(πΉβπ))) |
29 | | fthmon.h |
. . . . . . . 8
β’ π» = (Hom βπΆ) |
30 | 16, 29, 3, 17, 25, 20 | funcf2 17759 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (π§πΊπ):(π§π»π)βΆ((πΉβπ§)(Hom βπ·)(πΉβπ))) |
31 | | simpr2 1196 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π β (π§π»π)) |
32 | 30, 31 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((π§πΊπ)βπ) β ((πΉβπ§)(Hom βπ·)(πΉβπ))) |
33 | | simpr3 1197 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π β (π§π»π)) |
34 | 30, 33 | ffvelcdmd 7037 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((π§πΊπ)βπ) β ((πΉβπ§)(Hom βπ·)(πΉβπ))) |
35 | 2, 3, 4, 5, 15, 21, 24, 26, 28, 32, 34 | moni 17624 |
. . . . 5
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ)) = (((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ)) β ((π§πΊπ)βπ) = ((π§πΊπ)βπ))) |
36 | | eqid 2733 |
. . . . . . . 8
β’
(compβπΆ) =
(compβπΆ) |
37 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β π
β (ππ»π)) |
38 | 16, 29, 36, 4, 17, 25, 20, 23, 31, 37 | funcco 17762 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((π§πΊπ)β(π
(β¨π§, πβ©(compβπΆ)π)π)) = (((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ))) |
39 | 16, 29, 36, 4, 17, 25, 20, 23, 33, 37 | funcco 17762 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((π§πΊπ)β(π
(β¨π§, πβ©(compβπΆ)π)π)) = (((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ))) |
40 | 38, 39 | eqeq12d 2749 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (((π§πΊπ)β(π
(β¨π§, πβ©(compβπΆ)π)π)) = ((π§πΊπ)β(π
(β¨π§, πβ©(compβπΆ)π)π)) β (((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ)) = (((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ)))) |
41 | 6 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β πΉ(πΆ Faith π·)πΊ) |
42 | 13 | simpld 496 |
. . . . . . . . 9
β’ (π β πΆ β Cat) |
43 | 42 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β πΆ β Cat) |
44 | 16, 29, 36, 43, 25, 20, 23, 31, 37 | catcocl 17570 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (π
(β¨π§, πβ©(compβπΆ)π)π) β (π§π»π)) |
45 | 16, 29, 36, 43, 25, 20, 23, 33, 37 | catcocl 17570 |
. . . . . . 7
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (π
(β¨π§, πβ©(compβπΆ)π)π) β (π§π»π)) |
46 | 16, 29, 3, 41, 25, 23, 44, 45 | fthi 17810 |
. . . . . 6
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (((π§πΊπ)β(π
(β¨π§, πβ©(compβπΆ)π)π)) = ((π§πΊπ)β(π
(β¨π§, πβ©(compβπΆ)π)π)) β (π
(β¨π§, πβ©(compβπΆ)π)π) = (π
(β¨π§, πβ©(compβπΆ)π)π))) |
47 | 40, 46 | bitr3d 281 |
. . . . 5
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ)) = (((ππΊπ)βπ
)(β¨(πΉβπ§), (πΉβπ)β©(compβπ·)(πΉβπ))((π§πΊπ)βπ)) β (π
(β¨π§, πβ©(compβπΆ)π)π) = (π
(β¨π§, πβ©(compβπΆ)π)π))) |
48 | 16, 29, 3, 41, 25, 20, 31, 33 | fthi 17810 |
. . . . 5
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β (((π§πΊπ)βπ) = ((π§πΊπ)βπ) β π = π)) |
49 | 35, 47, 48 | 3bitr3d 309 |
. . . 4
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((π
(β¨π§, πβ©(compβπΆ)π)π) = (π
(β¨π§, πβ©(compβπΆ)π)π) β π = π)) |
50 | 49 | biimpd 228 |
. . 3
β’ ((π β§ (π§ β π΅ β§ π β (π§π»π) β§ π β (π§π»π))) β ((π
(β¨π§, πβ©(compβπΆ)π)π) = (π
(β¨π§, πβ©(compβπΆ)π)π) β π = π)) |
51 | 50 | ralrimivvva 3197 |
. 2
β’ (π β βπ§ β π΅ βπ β (π§π»π)βπ β (π§π»π)((π
(β¨π§, πβ©(compβπΆ)π)π) = (π
(β¨π§, πβ©(compβπΆ)π)π) β π = π)) |
52 | | fthmon.m |
. . 3
β’ π = (MonoβπΆ) |
53 | 16, 29, 36, 52, 42, 19, 22 | ismon2 17622 |
. 2
β’ (π β (π
β (πππ) β (π
β (ππ»π) β§ βπ§ β π΅ βπ β (π§π»π)βπ β (π§π»π)((π
(β¨π§, πβ©(compβπΆ)π)π) = (π
(β¨π§, πβ©(compβπΆ)π)π) β π = π)))) |
54 | 1, 51, 53 | mpbir2and 712 |
1
β’ (π β π
β (πππ)) |