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 ) ) ) >. )