Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(BaseβπΆ) =
(BaseβπΆ) |
2 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (Hom
βπΆ) = (Hom
βπΆ) |
3 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (Hom
βπ·) = (Hom
βπ·) |
4 | | monpropd.3 |
. . . . . . . . . . . . . 14
β’ (π β (Homf
βπΆ) =
(Homf βπ·)) |
5 | 4 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β (Homf
βπΆ) =
(Homf βπ·)) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β (Homf
βπΆ) =
(Homf βπ·)) |
7 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
8 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
9 | 1, 2, 3, 6, 7, 8 | homfeqval 17641 |
. . . . . . . . . . 11
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β (π(Hom βπΆ)π) = (π(Hom βπ·)π)) |
10 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(compβπΆ) =
(compβπΆ) |
11 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(compβπ·) =
(compβπ·) |
12 | 4 | ad5antr 733 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β (Homf
βπΆ) =
(Homf βπ·)) |
13 | | monpropd.4 |
. . . . . . . . . . . . 13
β’ (π β
(compfβπΆ) = (compfβπ·)) |
14 | 13 | ad5antr 733 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β
(compfβπΆ) = (compfβπ·)) |
15 | | simplr 768 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β π β (BaseβπΆ)) |
16 | | simp-5r 785 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β π β (BaseβπΆ)) |
17 | | simp-4r 783 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β π β (BaseβπΆ)) |
18 | | simpr 486 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β π β (π(Hom βπΆ)π)) |
19 | | simpllr 775 |
. . . . . . . . . . . 12
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β π β (π(Hom βπΆ)π)) |
20 | 1, 2, 10, 11, 12, 14, 15, 16, 17, 18, 19 | comfeqval 17652 |
. . . . . . . . . . 11
β’
((((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β (π(β¨π, πβ©(compβπΆ)π)π) = (π(β¨π, πβ©(compβπ·)π)π)) |
21 | 9, 20 | mpteq12dva 5238 |
. . . . . . . . . 10
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β (π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π)) = (π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))) |
22 | 21 | cnveqd 5876 |
. . . . . . . . 9
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π)) = β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))) |
23 | 22 | funeqd 6571 |
. . . . . . . 8
β’
(((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β§ π β (BaseβπΆ)) β (Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π)) β Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π)))) |
24 | 23 | ralbidva 3176 |
. . . . . . 7
β’ ((((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β§ π β (π(Hom βπΆ)π)) β (βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π)) β βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π)))) |
25 | 24 | rabbidva 3440 |
. . . . . 6
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π))} = {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))}) |
26 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
27 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β π β (BaseβπΆ)) |
28 | 1, 2, 3, 5, 26, 27 | homfeqval 17641 |
. . . . . . 7
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β (π(Hom βπΆ)π) = (π(Hom βπ·)π)) |
29 | 4 | homfeqbas 17640 |
. . . . . . . . 9
β’ (π β (BaseβπΆ) = (Baseβπ·)) |
30 | 29 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β (BaseβπΆ) = (Baseβπ·)) |
31 | 30 | raleqdv 3326 |
. . . . . . 7
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β (βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π)) β βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π)))) |
32 | 28, 31 | rabeqbidv 3450 |
. . . . . 6
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))} = {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))}) |
33 | 25, 32 | eqtrd 2773 |
. . . . 5
β’ (((π β§ π β (BaseβπΆ)) β§ π β (BaseβπΆ)) β {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π))} = {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))}) |
34 | 33 | 3impa 1111 |
. . . 4
β’ ((π β§ π β (BaseβπΆ) β§ π β (BaseβπΆ)) β {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π))} = {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))}) |
35 | 34 | mpoeq3dva 7486 |
. . 3
β’ (π β (π β (BaseβπΆ), π β (BaseβπΆ) β¦ {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π))}) = (π β (BaseβπΆ), π β (BaseβπΆ) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))})) |
36 | | mpoeq12 7482 |
. . . 4
β’
(((BaseβπΆ) =
(Baseβπ·) β§
(BaseβπΆ) =
(Baseβπ·)) β
(π β (BaseβπΆ), π β (BaseβπΆ) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))}) = (π β (Baseβπ·), π β (Baseβπ·) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))})) |
37 | 29, 29, 36 | syl2anc 585 |
. . 3
β’ (π β (π β (BaseβπΆ), π β (BaseβπΆ) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))}) = (π β (Baseβπ·), π β (Baseβπ·) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))})) |
38 | 35, 37 | eqtrd 2773 |
. 2
β’ (π β (π β (BaseβπΆ), π β (BaseβπΆ) β¦ {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π))}) = (π β (Baseβπ·), π β (Baseβπ·) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))})) |
39 | | eqid 2733 |
. . 3
β’
(MonoβπΆ) =
(MonoβπΆ) |
40 | | monpropd.c |
. . 3
β’ (π β πΆ β Cat) |
41 | 1, 2, 10, 39, 40 | monfval 17679 |
. 2
β’ (π β (MonoβπΆ) = (π β (BaseβπΆ), π β (BaseβπΆ) β¦ {π β (π(Hom βπΆ)π) β£ βπ β (BaseβπΆ)Fun β‘(π β (π(Hom βπΆ)π) β¦ (π(β¨π, πβ©(compβπΆ)π)π))})) |
42 | | eqid 2733 |
. . 3
β’
(Baseβπ·) =
(Baseβπ·) |
43 | | eqid 2733 |
. . 3
β’
(Monoβπ·) =
(Monoβπ·) |
44 | | monpropd.d |
. . 3
β’ (π β π· β Cat) |
45 | 42, 3, 11, 43, 44 | monfval 17679 |
. 2
β’ (π β (Monoβπ·) = (π β (Baseβπ·), π β (Baseβπ·) β¦ {π β (π(Hom βπ·)π) β£ βπ β (Baseβπ·)Fun β‘(π β (π(Hom βπ·)π) β¦ (π(β¨π, πβ©(compβπ·)π)π))})) |
46 | 38, 41, 45 | 3eqtr4d 2783 |
1
β’ (π β (MonoβπΆ) = (Monoβπ·)) |