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	syl5bb	|- ( ph -> ( F ( S Func C ) G <-> ( idFunc ` S ) e. ( S Func C ) ) )
18	10 17	mpbird	|- ( ph -> F ( S Func C ) G )