Step | Hyp | Ref
| Expression |
1 | | orc 866 |
. . 3
β’ (πΉ(πΆ Func π·)πΊ β (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) |
2 | 1 | a1i 11 |
. 2
β’ (π β (πΉ(πΆ Func π·)πΊ β (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ))) |
3 | | olc 867 |
. . 3
β’ (πΉ(πΆ Func πΈ)πΊ β (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) |
4 | 3 | a1i 11 |
. 2
β’ (π β (πΉ(πΆ Func πΈ)πΊ β (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ))) |
5 | | funcres2c.a |
. . . . 5
β’ π΄ = (BaseβπΆ) |
6 | | eqid 2733 |
. . . . 5
β’ (Hom
βπΆ) = (Hom
βπΆ) |
7 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ·) =
(Baseβπ·) |
8 | | eqid 2733 |
. . . . . . 7
β’
(Homf βπ·) = (Homf βπ·) |
9 | | funcres2c.d |
. . . . . . 7
β’ (π β π· β Cat) |
10 | | inss2 4190 |
. . . . . . . 8
β’ (π β© (Baseβπ·)) β (Baseβπ·) |
11 | 10 | a1i 11 |
. . . . . . 7
β’ (π β (π β© (Baseβπ·)) β (Baseβπ·)) |
12 | 7, 8, 9, 11 | fullsubc 17741 |
. . . . . 6
β’ (π β ((Homf
βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) β (Subcatβπ·)) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β ((Homf
βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) β (Subcatβπ·)) |
14 | 8, 7 | homffn 17578 |
. . . . . . 7
β’
(Homf βπ·) Fn ((Baseβπ·) Γ (Baseβπ·)) |
15 | | xpss12 5649 |
. . . . . . . 8
β’ (((π β© (Baseβπ·)) β (Baseβπ·) β§ (π β© (Baseβπ·)) β (Baseβπ·)) β ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))) β ((Baseβπ·) Γ (Baseβπ·))) |
16 | 10, 10, 15 | mp2an 691 |
. . . . . . 7
β’ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))) β ((Baseβπ·) Γ (Baseβπ·)) |
17 | | fnssres 6625 |
. . . . . . 7
β’
(((Homf βπ·) Fn ((Baseβπ·) Γ (Baseβπ·)) β§ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))) β ((Baseβπ·) Γ (Baseβπ·))) β ((Homf
βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) Fn ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) |
18 | 14, 16, 17 | mp2an 691 |
. . . . . 6
β’
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) Fn ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))) |
19 | 18 | a1i 11 |
. . . . 5
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β ((Homf
βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) Fn ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))) |
20 | | funcres2c.1 |
. . . . . . . 8
β’ (π β πΉ:π΄βΆπ) |
21 | 20 | adantr 482 |
. . . . . . 7
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β πΉ:π΄βΆπ) |
22 | 21 | ffnd 6670 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β πΉ Fn π΄) |
23 | 21 | frnd 6677 |
. . . . . . 7
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β ran πΉ β π) |
24 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ πΉ(πΆ Func π·)πΊ) β πΉ(πΆ Func π·)πΊ) |
25 | 5, 7, 24 | funcf1 17757 |
. . . . . . . . 9
β’ ((π β§ πΉ(πΆ Func π·)πΊ) β πΉ:π΄βΆ(Baseβπ·)) |
26 | 25 | frnd 6677 |
. . . . . . . 8
β’ ((π β§ πΉ(πΆ Func π·)πΊ) β ran πΉ β (Baseβπ·)) |
27 | | eqid 2733 |
. . . . . . . . . . 11
β’
(BaseβπΈ) =
(BaseβπΈ) |
28 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ πΉ(πΆ Func πΈ)πΊ) β πΉ(πΆ Func πΈ)πΊ) |
29 | 5, 27, 28 | funcf1 17757 |
. . . . . . . . . 10
β’ ((π β§ πΉ(πΆ Func πΈ)πΊ) β πΉ:π΄βΆ(BaseβπΈ)) |
30 | 29 | frnd 6677 |
. . . . . . . . 9
β’ ((π β§ πΉ(πΆ Func πΈ)πΊ) β ran πΉ β (BaseβπΈ)) |
31 | | funcres2c.e |
. . . . . . . . . 10
β’ πΈ = (π· βΎs π) |
32 | 31, 7 | ressbasss 17126 |
. . . . . . . . 9
β’
(BaseβπΈ)
β (Baseβπ·) |
33 | 30, 32 | sstrdi 3957 |
. . . . . . . 8
β’ ((π β§ πΉ(πΆ Func πΈ)πΊ) β ran πΉ β (Baseβπ·)) |
34 | 26, 33 | jaodan 957 |
. . . . . . 7
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β ran πΉ β (Baseβπ·)) |
35 | 23, 34 | ssind 4193 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β ran πΉ β (π β© (Baseβπ·))) |
36 | | df-f 6501 |
. . . . . 6
β’ (πΉ:π΄βΆ(π β© (Baseβπ·)) β (πΉ Fn π΄ β§ ran πΉ β (π β© (Baseβπ·)))) |
37 | 22, 35, 36 | sylanbrc 584 |
. . . . 5
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β πΉ:π΄βΆ(π β© (Baseβπ·))) |
38 | | eqid 2733 |
. . . . . . . . 9
β’ (Hom
βπ·) = (Hom
βπ·) |
39 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func π·)πΊ) β πΉ(πΆ Func π·)πΊ) |
40 | | simplrl 776 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func π·)πΊ) β π₯ β π΄) |
41 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func π·)πΊ) β π¦ β π΄) |
42 | 5, 6, 38, 39, 40, 41 | funcf2 17759 |
. . . . . . . 8
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func π·)πΊ) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
43 | | eqid 2733 |
. . . . . . . . . 10
β’ (Hom
βπΈ) = (Hom
βπΈ) |
44 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β πΉ(πΆ Func πΈ)πΊ) |
45 | | simplrl 776 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β π₯ β π΄) |
46 | | simplrr 777 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β π¦ β π΄) |
47 | 5, 6, 43, 44, 45, 46 | funcf2 17759 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπΈ)(πΉβπ¦))) |
48 | | funcres2c.r |
. . . . . . . . . . . . 13
β’ (π β π β π) |
49 | 31, 38 | resshom 17305 |
. . . . . . . . . . . . 13
β’ (π β π β (Hom βπ·) = (Hom βπΈ)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (Hom βπ·) = (Hom βπΈ)) |
51 | 50 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β (Hom βπ·) = (Hom βπΈ)) |
52 | 51 | oveqd 7375 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) = ((πΉβπ₯)(Hom βπΈ)(πΉβπ¦))) |
53 | 52 | feq3d 6656 |
. . . . . . . . 9
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β ((π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπΈ)(πΉβπ¦)))) |
54 | 47, 53 | mpbird 257 |
. . . . . . . 8
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ πΉ(πΆ Func πΈ)πΊ) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
55 | 42, 54 | jaodan 957 |
. . . . . . 7
β’ (((π β§ (π₯ β π΄ β§ π¦ β π΄)) β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
56 | 55 | an32s 651 |
. . . . . 6
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
57 | 37 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β πΉ:π΄βΆ(π β© (Baseβπ·))) |
58 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β π₯ β π΄) |
59 | 57, 58 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β (πΉβπ₯) β (π β© (Baseβπ·))) |
60 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β π¦ β π΄) |
61 | 57, 60 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β (πΉβπ¦) β (π β© (Baseβπ·))) |
62 | 59, 61 | ovresd 7522 |
. . . . . . . 8
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πΉβπ₯)((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))(πΉβπ¦)) = ((πΉβπ₯)(Homf βπ·)(πΉβπ¦))) |
63 | 59 | elin2d 4160 |
. . . . . . . . 9
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β (πΉβπ₯) β (Baseβπ·)) |
64 | 61 | elin2d 4160 |
. . . . . . . . 9
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β (πΉβπ¦) β (Baseβπ·)) |
65 | 8, 7, 38, 63, 64 | homfval 17577 |
. . . . . . . 8
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πΉβπ₯)(Homf βπ·)(πΉβπ¦)) = ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
66 | 62, 65 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((πΉβπ₯)((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))(πΉβπ¦)) = ((πΉβπ₯)(Hom βπ·)(πΉβπ¦))) |
67 | 66 | feq3d 6656 |
. . . . . 6
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β ((π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))(πΉβπ¦)) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)(Hom βπ·)(πΉβπ¦)))) |
68 | 56, 67 | mpbird 257 |
. . . . 5
β’ (((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β§ (π₯ β π΄ β§ π¦ β π΄)) β (π₯πΊπ¦):(π₯(Hom βπΆ)π¦)βΆ((πΉβπ₯)((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))(πΉβπ¦))) |
69 | 5, 6, 13, 19, 37, 68 | funcres2b 17788 |
. . . 4
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func (π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))πΊ)) |
70 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (Homf
βπΆ) =
(Homf βπΆ)) |
71 | | eqidd 2734 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β
(compfβπΆ) = (compfβπΆ)) |
72 | 7 | ressinbas 17131 |
. . . . . . . . . . 11
β’ (π β π β (π· βΎs π) = (π· βΎs (π β© (Baseβπ·)))) |
73 | 48, 72 | syl 17 |
. . . . . . . . . 10
β’ (π β (π· βΎs π) = (π· βΎs (π β© (Baseβπ·)))) |
74 | 31, 73 | eqtrid 2785 |
. . . . . . . . 9
β’ (π β πΈ = (π· βΎs (π β© (Baseβπ·)))) |
75 | 74 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (Homf
βπΈ) =
(Homf β(π· βΎs (π β© (Baseβπ·))))) |
76 | | eqid 2733 |
. . . . . . . . . 10
β’ (π· βΎs (π β© (Baseβπ·))) = (π· βΎs (π β© (Baseβπ·))) |
77 | | eqid 2733 |
. . . . . . . . . 10
β’ (π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))) = (π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))) |
78 | 7, 8, 9, 11, 76, 77 | fullresc 17742 |
. . . . . . . . 9
β’ (π β ((Homf
β(π·
βΎs (π
β© (Baseβπ·)))) =
(Homf β(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))))) β§
(compfβ(π· βΎs (π β© (Baseβπ·)))) = (compfβ(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·)))))))) |
79 | 78 | simpld 496 |
. . . . . . . 8
β’ (π β (Homf
β(π·
βΎs (π
β© (Baseβπ·)))) =
(Homf β(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
80 | 75, 79 | eqtrd 2773 |
. . . . . . 7
β’ (π β (Homf
βπΈ) =
(Homf β(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
81 | 80 | adantr 482 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (Homf
βπΈ) =
(Homf β(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
82 | 74 | fveq2d 6847 |
. . . . . . . 8
β’ (π β
(compfβπΈ) = (compfβ(π· βΎs (π β© (Baseβπ·))))) |
83 | 78 | simprd 497 |
. . . . . . . 8
β’ (π β
(compfβ(π· βΎs (π β© (Baseβπ·)))) = (compfβ(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
84 | 82, 83 | eqtrd 2773 |
. . . . . . 7
β’ (π β
(compfβπΈ) = (compfβ(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
85 | 84 | adantr 482 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β
(compfβπΈ) = (compfβ(π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
86 | | df-br 5107 |
. . . . . . . . . . 11
β’ (πΉ(πΆ Func π·)πΊ β β¨πΉ, πΊβ© β (πΆ Func π·)) |
87 | | funcrcl 17754 |
. . . . . . . . . . 11
β’
(β¨πΉ, πΊβ© β (πΆ Func π·) β (πΆ β Cat β§ π· β Cat)) |
88 | 86, 87 | sylbi 216 |
. . . . . . . . . 10
β’ (πΉ(πΆ Func π·)πΊ β (πΆ β Cat β§ π· β Cat)) |
89 | 88 | simpld 496 |
. . . . . . . . 9
β’ (πΉ(πΆ Func π·)πΊ β πΆ β Cat) |
90 | | df-br 5107 |
. . . . . . . . . . 11
β’ (πΉ(πΆ Func πΈ)πΊ β β¨πΉ, πΊβ© β (πΆ Func πΈ)) |
91 | | funcrcl 17754 |
. . . . . . . . . . 11
β’
(β¨πΉ, πΊβ© β (πΆ Func πΈ) β (πΆ β Cat β§ πΈ β Cat)) |
92 | 90, 91 | sylbi 216 |
. . . . . . . . . 10
β’ (πΉ(πΆ Func πΈ)πΊ β (πΆ β Cat β§ πΈ β Cat)) |
93 | 92 | simpld 496 |
. . . . . . . . 9
β’ (πΉ(πΆ Func πΈ)πΊ β πΆ β Cat) |
94 | 89, 93 | jaoi 856 |
. . . . . . . 8
β’ ((πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ) β πΆ β Cat) |
95 | 94 | elexd 3464 |
. . . . . . 7
β’ ((πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ) β πΆ β V) |
96 | 95 | adantl 483 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β πΆ β V) |
97 | 31 | ovexi 7392 |
. . . . . . 7
β’ πΈ β V |
98 | 97 | a1i 11 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β πΈ β V) |
99 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))) β V) |
100 | 70, 71, 81, 85, 96, 96, 98, 99 | funcpropd 17792 |
. . . . 5
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (πΆ Func πΈ) = (πΆ Func (π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))) |
101 | 100 | breqd 5117 |
. . . 4
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (πΉ(πΆ Func πΈ)πΊ β πΉ(πΆ Func (π· βΎcat
((Homf βπ·) βΎ ((π β© (Baseβπ·)) Γ (π β© (Baseβπ·))))))πΊ)) |
102 | 69, 101 | bitr4d 282 |
. . 3
β’ ((π β§ (πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ)) β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func πΈ)πΊ)) |
103 | 102 | ex 414 |
. 2
β’ (π β ((πΉ(πΆ Func π·)πΊ β¨ πΉ(πΆ Func πΈ)πΊ) β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func πΈ)πΊ))) |
104 | 2, 4, 103 | pm5.21ndd 381 |
1
β’ (π β (πΉ(πΆ Func π·)πΊ β πΉ(πΆ Func πΈ)πΊ)) |