Step | Hyp | Ref
| Expression |
1 | | relfunc 17753 |
. . 3
β’ Rel
(π· Func π·) |
2 | | ressffth.d |
. . . . 5
β’ π· = (πΆ βΎs π) |
3 | | resscat 17743 |
. . . . 5
β’ ((πΆ β Cat β§ π β π) β (πΆ βΎs π) β Cat) |
4 | 2, 3 | eqeltrid 2838 |
. . . 4
β’ ((πΆ β Cat β§ π β π) β π· β Cat) |
5 | | ressffth.i |
. . . . 5
β’ πΌ =
(idfuncβπ·) |
6 | 5 | idfucl 17772 |
. . . 4
β’ (π· β Cat β πΌ β (π· Func π·)) |
7 | 4, 6 | syl 17 |
. . 3
β’ ((πΆ β Cat β§ π β π) β πΌ β (π· Func π·)) |
8 | | 1st2nd 7972 |
. . 3
β’ ((Rel
(π· Func π·) β§ πΌ β (π· Func π·)) β πΌ = β¨(1st βπΌ), (2nd βπΌ)β©) |
9 | 1, 7, 8 | sylancr 588 |
. 2
β’ ((πΆ β Cat β§ π β π) β πΌ = β¨(1st βπΌ), (2nd βπΌ)β©) |
10 | | eqidd 2734 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β (Homf
βπ·) =
(Homf βπ·)) |
11 | | eqidd 2734 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β
(compfβπ·) = (compfβπ·)) |
12 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(BaseβπΆ) =
(BaseβπΆ) |
13 | 12 | ressinbas 17131 |
. . . . . . . . . . . . 13
β’ (π β π β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
14 | 13 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΆ β Cat β§ π β π) β (πΆ βΎs π) = (πΆ βΎs (π β© (BaseβπΆ)))) |
15 | 2, 14 | eqtrid 2785 |
. . . . . . . . . . 11
β’ ((πΆ β Cat β§ π β π) β π· = (πΆ βΎs (π β© (BaseβπΆ)))) |
16 | 15 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((πΆ β Cat β§ π β π) β (Homf
βπ·) =
(Homf β(πΆ βΎs (π β© (BaseβπΆ))))) |
17 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Homf βπΆ) = (Homf βπΆ) |
18 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((πΆ β Cat β§ π β π) β πΆ β Cat) |
19 | | inss2 4190 |
. . . . . . . . . . . . 13
β’ (π β© (BaseβπΆ)) β (BaseβπΆ) |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
β’ ((πΆ β Cat β§ π β π) β (π β© (BaseβπΆ)) β (BaseβπΆ)) |
21 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (πΆ βΎs (π β© (BaseβπΆ))) = (πΆ βΎs (π β© (BaseβπΆ))) |
22 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))) = (πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))) |
23 | 12, 17, 18, 20, 21, 22 | fullresc 17742 |
. . . . . . . . . . 11
β’ ((πΆ β Cat β§ π β π) β ((Homf
β(πΆ
βΎs (π
β© (BaseβπΆ)))) =
(Homf β(πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ)))))) β§
(compfβ(πΆ βΎs (π β© (BaseβπΆ)))) = (compfβ(πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ)))))))) |
24 | 23 | simpld 496 |
. . . . . . . . . 10
β’ ((πΆ β Cat β§ π β π) β (Homf
β(πΆ
βΎs (π
β© (BaseβπΆ)))) =
(Homf β(πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))))) |
25 | 16, 24 | eqtrd 2773 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β (Homf
βπ·) =
(Homf β(πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))))) |
26 | 15 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((πΆ β Cat β§ π β π) β
(compfβπ·) = (compfβ(πΆ βΎs (π β© (BaseβπΆ))))) |
27 | 23 | simprd 497 |
. . . . . . . . . 10
β’ ((πΆ β Cat β§ π β π) β
(compfβ(πΆ βΎs (π β© (BaseβπΆ)))) = (compfβ(πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))))) |
28 | 26, 27 | eqtrd 2773 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β
(compfβπ·) = (compfβ(πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))))) |
29 | 2 | ovexi 7392 |
. . . . . . . . . 10
β’ π· β V |
30 | 29 | a1i 11 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β π· β V) |
31 | | ovexd 7393 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β (πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))) β V) |
32 | 10, 11, 25, 28, 30, 30, 30, 31 | funcpropd 17792 |
. . . . . . . 8
β’ ((πΆ β Cat β§ π β π) β (π· Func π·) = (π· Func (πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ))))))) |
33 | 12, 17, 18, 20 | fullsubc 17741 |
. . . . . . . . 9
β’ ((πΆ β Cat β§ π β π) β ((Homf
βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ)))) β (SubcatβπΆ)) |
34 | | funcres2 17789 |
. . . . . . . . 9
β’
(((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ)))) β (SubcatβπΆ) β (π· Func (πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ)))))) β (π· Func πΆ)) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
β’ ((πΆ β Cat β§ π β π) β (π· Func (πΆ βΎcat
((Homf βπΆ) βΎ ((π β© (BaseβπΆ)) Γ (π β© (BaseβπΆ)))))) β (π· Func πΆ)) |
36 | 32, 35 | eqsstrd 3983 |
. . . . . . 7
β’ ((πΆ β Cat β§ π β π) β (π· Func π·) β (π· Func πΆ)) |
37 | 36, 7 | sseldd 3946 |
. . . . . 6
β’ ((πΆ β Cat β§ π β π) β πΌ β (π· Func πΆ)) |
38 | 9, 37 | eqeltrrd 2835 |
. . . . 5
β’ ((πΆ β Cat β§ π β π) β β¨(1st βπΌ), (2nd βπΌ)β© β (π· Func πΆ)) |
39 | | df-br 5107 |
. . . . 5
β’
((1st βπΌ)(π· Func πΆ)(2nd βπΌ) β β¨(1st βπΌ), (2nd βπΌ)β© β (π· Func πΆ)) |
40 | 38, 39 | sylibr 233 |
. . . 4
β’ ((πΆ β Cat β§ π β π) β (1st βπΌ)(π· Func πΆ)(2nd βπΌ)) |
41 | | f1oi 6823 |
. . . . . 6
β’ ( I
βΎ (π₯(Hom βπ·)π¦)):(π₯(Hom βπ·)π¦)β1-1-ontoβ(π₯(Hom βπ·)π¦) |
42 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβπ·) =
(Baseβπ·) |
43 | 4 | adantr 482 |
. . . . . . . 8
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β π· β Cat) |
44 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
βπ·) = (Hom
βπ·) |
45 | | simprl 770 |
. . . . . . . 8
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β π₯ β (Baseβπ·)) |
46 | | simprr 772 |
. . . . . . . 8
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β π¦ β (Baseβπ·)) |
47 | 5, 42, 43, 44, 45, 46 | idfu2nd 17768 |
. . . . . . 7
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β (π₯(2nd βπΌ)π¦) = ( I βΎ (π₯(Hom βπ·)π¦))) |
48 | | eqidd 2734 |
. . . . . . 7
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β (π₯(Hom βπ·)π¦) = (π₯(Hom βπ·)π¦)) |
49 | | eqid 2733 |
. . . . . . . . . 10
β’ (Hom
βπΆ) = (Hom
βπΆ) |
50 | 2, 49 | resshom 17305 |
. . . . . . . . 9
β’ (π β π β (Hom βπΆ) = (Hom βπ·)) |
51 | 50 | ad2antlr 726 |
. . . . . . . 8
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β (Hom βπΆ) = (Hom βπ·)) |
52 | 5, 42, 43, 45 | idfu1 17771 |
. . . . . . . 8
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β ((1st βπΌ)βπ₯) = π₯) |
53 | 5, 42, 43, 46 | idfu1 17771 |
. . . . . . . 8
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β ((1st βπΌ)βπ¦) = π¦) |
54 | 51, 52, 53 | oveq123d 7379 |
. . . . . . 7
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β (((1st βπΌ)βπ₯)(Hom βπΆ)((1st βπΌ)βπ¦)) = (π₯(Hom βπ·)π¦)) |
55 | 47, 48, 54 | f1oeq123d 6779 |
. . . . . 6
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β ((π₯(2nd βπΌ)π¦):(π₯(Hom βπ·)π¦)β1-1-ontoβ(((1st βπΌ)βπ₯)(Hom βπΆ)((1st βπΌ)βπ¦)) β ( I βΎ (π₯(Hom βπ·)π¦)):(π₯(Hom βπ·)π¦)β1-1-ontoβ(π₯(Hom βπ·)π¦))) |
56 | 41, 55 | mpbiri 258 |
. . . . 5
β’ (((πΆ β Cat β§ π β π) β§ (π₯ β (Baseβπ·) β§ π¦ β (Baseβπ·))) β (π₯(2nd βπΌ)π¦):(π₯(Hom βπ·)π¦)β1-1-ontoβ(((1st βπΌ)βπ₯)(Hom βπΆ)((1st βπΌ)βπ¦))) |
57 | 56 | ralrimivva 3194 |
. . . 4
β’ ((πΆ β Cat β§ π β π) β βπ₯ β (Baseβπ·)βπ¦ β (Baseβπ·)(π₯(2nd βπΌ)π¦):(π₯(Hom βπ·)π¦)β1-1-ontoβ(((1st βπΌ)βπ₯)(Hom βπΆ)((1st βπΌ)βπ¦))) |
58 | 42, 44, 49 | isffth2 17808 |
. . . 4
β’
((1st βπΌ)((π· Full πΆ) β© (π· Faith πΆ))(2nd βπΌ) β ((1st βπΌ)(π· Func πΆ)(2nd βπΌ) β§ βπ₯ β (Baseβπ·)βπ¦ β (Baseβπ·)(π₯(2nd βπΌ)π¦):(π₯(Hom βπ·)π¦)β1-1-ontoβ(((1st βπΌ)βπ₯)(Hom βπΆ)((1st βπΌ)βπ¦)))) |
59 | 40, 57, 58 | sylanbrc 584 |
. . 3
β’ ((πΆ β Cat β§ π β π) β (1st βπΌ)((π· Full πΆ) β© (π· Faith πΆ))(2nd βπΌ)) |
60 | | df-br 5107 |
. . 3
β’
((1st βπΌ)((π· Full πΆ) β© (π· Faith πΆ))(2nd βπΌ) β β¨(1st βπΌ), (2nd βπΌ)β© β ((π· Full πΆ) β© (π· Faith πΆ))) |
61 | 59, 60 | sylib 217 |
. 2
β’ ((πΆ β Cat β§ π β π) β β¨(1st βπΌ), (2nd βπΌ)β© β ((π· Full πΆ) β© (π· Faith πΆ))) |
62 | 9, 61 | eqeltrd 2834 |
1
β’ ((πΆ β Cat β§ π β π) β πΌ β ((π· Full πΆ) β© (π· Faith πΆ))) |