This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> J e. ( Subcat ` C ) )
inclfusubc.s 
|- S = ( C |`cat J )
inclfusubc.b 
|- B = ( Base ` S )
inclfusubc.f 
|- ( ph -> F = ( _I |` B ) )
inclfusubc.g 
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) )
Assertion inclfusubc 
|- ( ph -> F ( S Func C ) G )

Proof

Step Hyp Ref Expression
1 inclfusubc.j 
 |-  ( ph -> J e. ( Subcat ` C ) )
2 inclfusubc.s 
 |-  S = ( C |`cat J )
3 inclfusubc.b 
 |-  B = ( Base ` S )
4 inclfusubc.f 
 |-  ( ph -> F = ( _I |` B ) )
5 inclfusubc.g 
 |-  ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) )
6 fthfunc 
 |-  ( S Faith C ) C_ ( S Func C )
7 eqid 
 |-  ( idFunc ` S ) = ( idFunc ` S )
8 2 7 rescfth 
 |-  ( J e. ( Subcat ` C ) -> ( idFunc ` S ) e. ( S Faith C ) )
9 1 8 syl 
 |-  ( ph -> ( idFunc ` S ) e. ( S Faith C ) )
10 6 9 sselid 
 |-  ( ph -> ( idFunc ` S ) e. ( S Func C ) )
11 df-br 
 |-  ( F ( S Func C ) G <-> <. F , G >. e. ( S Func C ) )
12 4 5 opeq12d 
 |-  ( ph -> <. F , G >. = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )
13 2 7 3 idfusubc 
 |-  ( J e. ( Subcat ` C ) -> ( idFunc ` S ) = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )
14 1 13 syl 
 |-  ( ph -> ( idFunc ` S ) = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )
15 12 14 eqtr4d 
 |-  ( ph -> <. F , G >. = ( idFunc ` S ) )
16 15 eleq1d 
 |-  ( ph -> ( <. F , G >. e. ( S Func C ) <-> ( idFunc ` S ) e. ( S Func C ) ) )
17 11 16 bitrid 
 |-  ( ph -> ( F ( S Func C ) G <-> ( idFunc ` S ) e. ( S Func C ) ) )
18 10 17 mpbird 
 |-  ( ph -> F ( S Func C ) G )