Metamath Proof Explorer


Theorem inclfusubc

Description: The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020)

Ref Expression
Hypotheses inclfusubc.j φ J Subcat C
inclfusubc.s S = C cat J
inclfusubc.b B = Base S
inclfusubc.f φ F = I B
inclfusubc.g φ G = x B , y B I x J y
Assertion inclfusubc φ F S Func C G

Proof

Step Hyp Ref Expression
1 inclfusubc.j φ J Subcat C
2 inclfusubc.s S = C cat J
3 inclfusubc.b B = Base S
4 inclfusubc.f φ F = I B
5 inclfusubc.g φ G = x B , y B I x J y
6 fthfunc S Faith C S Func C
7 eqid id func S = id func S
8 2 7 rescfth J Subcat C id func S S Faith C
9 1 8 syl φ id func S S Faith C
10 6 9 sseldi φ id func S S Func C
11 df-br F S Func C G F G S Func C
12 4 5 opeq12d φ F G = I B x B , y B I x J y
13 2 7 3 idfusubc J Subcat C id func S = I B x B , y B I x J y
14 1 13 syl φ id func S = I B x B , y B I x J y
15 12 14 eqtr4d φ F G = id func S
16 15 eleq1d φ F G S Func C id func S S Func C
17 11 16 syl5bb φ F S Func C G id func S S Func C
18 10 17 mpbird φ F S Func C G