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