Step | Hyp | Ref
| Expression |
1 | | relfunc 17753 |
. . 3
β’ Rel
(πΆ Func (π· βΎcat π
)) |
2 | 1 | a1i 11 |
. 2
β’ (π
β (Subcatβπ·) β Rel (πΆ Func (π· βΎcat π
))) |
3 | | simpr 486 |
. . . . 5
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π(πΆ Func (π· βΎcat π
))π) |
4 | | eqid 2733 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
5 | | eqid 2733 |
. . . . . 6
β’ (Hom
βπΆ) = (Hom
βπΆ) |
6 | | simpl 484 |
. . . . . 6
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π
β (Subcatβπ·)) |
7 | | eqidd 2734 |
. . . . . . 7
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β dom dom π
= dom dom π
) |
8 | 6, 7 | subcfn 17732 |
. . . . . 6
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π
Fn (dom dom π
Γ dom dom π
)) |
9 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(π·
βΎcat π
)) =
(Baseβ(π·
βΎcat π
)) |
10 | 4, 9, 3 | funcf1 17757 |
. . . . . . 7
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π:(BaseβπΆ)βΆ(Baseβ(π· βΎcat π
))) |
11 | | eqid 2733 |
. . . . . . . . 9
β’ (π· βΎcat π
) = (π· βΎcat π
) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ·) =
(Baseβπ·) |
13 | | subcrcl 17704 |
. . . . . . . . . 10
β’ (π
β (Subcatβπ·) β π· β Cat) |
14 | 13 | adantr 482 |
. . . . . . . . 9
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π· β Cat) |
15 | 6, 8, 12 | subcss1 17733 |
. . . . . . . . 9
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β dom dom π
β (Baseβπ·)) |
16 | 11, 12, 14, 8, 15 | rescbas 17717 |
. . . . . . . 8
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β dom dom π
= (Baseβ(π· βΎcat π
))) |
17 | 16 | feq3d 6656 |
. . . . . . 7
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β (π:(BaseβπΆ)βΆdom dom π
β π:(BaseβπΆ)βΆ(Baseβ(π· βΎcat π
)))) |
18 | 10, 17 | mpbird 257 |
. . . . . 6
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π:(BaseβπΆ)βΆdom dom π
) |
19 | | eqid 2733 |
. . . . . . . 8
β’ (Hom
β(π·
βΎcat π
)) =
(Hom β(π·
βΎcat π
)) |
20 | | simplr 768 |
. . . . . . . 8
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β π(πΆ Func (π· βΎcat π
))π) |
21 | | simprl 770 |
. . . . . . . 8
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β π₯ β (BaseβπΆ)) |
22 | | simprr 772 |
. . . . . . . 8
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β π¦ β (BaseβπΆ)) |
23 | 4, 5, 19, 20, 21, 22 | funcf2 17759 |
. . . . . . 7
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (π₯ππ¦):(π₯(Hom βπΆ)π¦)βΆ((πβπ₯)(Hom β(π· βΎcat π
))(πβπ¦))) |
24 | 11, 12, 14, 8, 15 | reschom 17719 |
. . . . . . . . . 10
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π
= (Hom β(π· βΎcat π
))) |
25 | 24 | adantr 482 |
. . . . . . . . 9
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β π
= (Hom β(π· βΎcat π
))) |
26 | 25 | oveqd 7375 |
. . . . . . . 8
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β ((πβπ₯)π
(πβπ¦)) = ((πβπ₯)(Hom β(π· βΎcat π
))(πβπ¦))) |
27 | 26 | feq3d 6656 |
. . . . . . 7
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β ((π₯ππ¦):(π₯(Hom βπΆ)π¦)βΆ((πβπ₯)π
(πβπ¦)) β (π₯ππ¦):(π₯(Hom βπΆ)π¦)βΆ((πβπ₯)(Hom β(π· βΎcat π
))(πβπ¦)))) |
28 | 23, 27 | mpbird 257 |
. . . . . 6
β’ (((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β§ (π₯ β (BaseβπΆ) β§ π¦ β (BaseβπΆ))) β (π₯ππ¦):(π₯(Hom βπΆ)π¦)βΆ((πβπ₯)π
(πβπ¦))) |
29 | 4, 5, 6, 8, 18, 28 | funcres2b 17788 |
. . . . 5
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β (π(πΆ Func π·)π β π(πΆ Func (π· βΎcat π
))π)) |
30 | 3, 29 | mpbird 257 |
. . . 4
β’ ((π
β (Subcatβπ·) β§ π(πΆ Func (π· βΎcat π
))π) β π(πΆ Func π·)π) |
31 | 30 | ex 414 |
. . 3
β’ (π
β (Subcatβπ·) β (π(πΆ Func (π· βΎcat π
))π β π(πΆ Func π·)π)) |
32 | | df-br 5107 |
. . 3
β’ (π(πΆ Func (π· βΎcat π
))π β β¨π, πβ© β (πΆ Func (π· βΎcat π
))) |
33 | | df-br 5107 |
. . 3
β’ (π(πΆ Func π·)π β β¨π, πβ© β (πΆ Func π·)) |
34 | 31, 32, 33 | 3imtr3g 295 |
. 2
β’ (π
β (Subcatβπ·) β (β¨π, πβ© β (πΆ Func (π· βΎcat π
)) β β¨π, πβ© β (πΆ Func π·))) |
35 | 2, 34 | relssdv 5745 |
1
β’ (π
β (Subcatβπ·) β (πΆ Func (π· βΎcat π
)) β (πΆ Func π·)) |