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

Metamath Proof Explorer

Theorem idfusubc

Description: The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020)

Ref Expression
Hypotheses idfusubc.s 
|- S = ( C |`cat J )
idfusubc.i 
|- I = ( idFunc ` S )
idfusubc.b 
|- B = ( Base ` S )
Assertion idfusubc 
|- ( J e. ( Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )

Proof

Step Hyp Ref Expression
1 idfusubc.s 
 |-  S = ( C |`cat J )
2 idfusubc.i 
 |-  I = ( idFunc ` S )
3 idfusubc.b 
 |-  B = ( Base ` S )
4 1 2 3 idfusubc0 
 |-  ( J e. ( Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) >. )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 subcrcl 
 |-  ( J e. ( Subcat ` C ) -> C e. Cat )
7 id 
 |-  ( J e. ( Subcat ` C ) -> J e. ( Subcat ` C ) )
8 eqidd 
 |-  ( J e. ( Subcat ` C ) -> dom dom J = dom dom J )
9 7 8 subcfn 
 |-  ( J e. ( Subcat ` C ) -> J Fn ( dom dom J X. dom dom J ) )
10 7 9 5 subcss1 
 |-  ( J e. ( Subcat ` C ) -> dom dom J C_ ( Base ` C ) )
11 1 5 6 9 10 reschom 
 |-  ( J e. ( Subcat ` C ) -> J = ( Hom ` S ) )
12 11 eqcomd 
 |-  ( J e. ( Subcat ` C ) -> ( Hom ` S ) = J )
13 12 oveqd 
 |-  ( J e. ( Subcat ` C ) -> ( x ( Hom ` S ) y ) = ( x J y ) )
14 13 reseq2d 
 |-  ( J e. ( Subcat ` C ) -> ( _I |` ( x ( Hom ` S ) y ) ) = ( _I |` ( x J y ) ) )
15 14 mpoeq3dv 
 |-  ( J e. ( Subcat ` C ) -> ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) = ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) )
16 15 opeq2d 
 |-  ( J e. ( Subcat ` C ) -> <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) >. = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )
17 4 16 eqtrd 
 |-  ( J e. ( Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x J y ) ) ) >. )