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

Metamath Proof Explorer

Theorem idfusubc0

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 idfusubc0 
|- ( J e. ( Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) 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 id 
 |-  ( J e. ( Subcat ` C ) -> J e. ( Subcat ` C ) )
5 1 4 subccat 
 |-  ( J e. ( Subcat ` C ) -> S e. Cat )
6 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
7 2 3 5 6 idfuval 
 |-  ( J e. ( Subcat ` C ) -> I = <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` S ) ` z ) ) ) >. )
8 fveq2 
 |-  ( z = <. x , y >. -> ( ( Hom ` S ) ` z ) = ( ( Hom ` S ) ` <. x , y >. ) )
9 df-ov 
 |-  ( x ( Hom ` S ) y ) = ( ( Hom ` S ) ` <. x , y >. )
10 8 9 eqtr4di 
 |-  ( z = <. x , y >. -> ( ( Hom ` S ) ` z ) = ( x ( Hom ` S ) y ) )
11 10 reseq2d 
 |-  ( z = <. x , y >. -> ( _I |` ( ( Hom ` S ) ` z ) ) = ( _I |` ( x ( Hom ` S ) y ) ) )
12 11 mpompt 
 |-  ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` S ) ` z ) ) ) = ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) )
13 12 a1i 
 |-  ( J e. ( Subcat ` C ) -> ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` S ) ` z ) ) ) = ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) )
14 13 opeq2d 
 |-  ( J e. ( Subcat ` C ) -> <. ( _I |` B ) , ( z e. ( B X. B ) |-> ( _I |` ( ( Hom ` S ) ` z ) ) ) >. = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) >. )
15 7 14 eqtrd 
 |-  ( J e. ( Subcat ` C ) -> I = <. ( _I |` B ) , ( x e. B , y e. B |-> ( _I |` ( x ( Hom ` S ) y ) ) ) >. )