Theorem ressffth

Description: The inclusion functor from a full subcategory is a full and faithful functor, see also remark 4.4(2) in Adamek p. 49. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	ressffth.d	|- D = ( C |`s S )
	ressffth.i	|- I = ( idFunc ` D )
Assertion	ressffth	|- ( ( C e. Cat /\ S e. V ) -> I e. ( ( D Full C ) i^i ( D Faith C ) ) )

Proof

Step	Hyp	Ref	Expression
1		ressffth.d	|- D = ( C |`s S )
2		ressffth.i	|- I = ( idFunc ` D )
3		relfunc	|- Rel ( D Func D )
4		resscat	|- ( ( C e. Cat /\ S e. V ) -> ( C |`s S ) e. Cat )
5	1 4	eqeltrid	|- ( ( C e. Cat /\ S e. V ) -> D e. Cat )
6	2	idfucl	|- ( D e. Cat -> I e. ( D Func D ) )
7	5 6	syl	|- ( ( C e. Cat /\ S e. V ) -> I e. ( D Func D ) )
8		1st2nd	|- ( ( Rel ( D Func D ) /\ I e. ( D Func D ) ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
9	3 7 8	sylancr	|- ( ( C e. Cat /\ S e. V ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
10		eqidd	|- ( ( C e. Cat /\ S e. V ) -> ( Homf ` D ) = ( Homf ` D ) )
11		eqidd	|- ( ( C e. Cat /\ S e. V ) -> ( comf ` D ) = ( comf ` D ) )
12		eqid	|- ( Base ` C ) = ( Base ` C )
13	12	ressinbas	|- ( S e. V -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
14	13	adantl	|- ( ( C e. Cat /\ S e. V ) -> ( C |`s S ) = ( C |`s ( S i^i ( Base ` C ) ) ) )
15	1 14	syl5eq	|- ( ( C e. Cat /\ S e. V ) -> D = ( C |`s ( S i^i ( Base ` C ) ) ) )
16	15	fveq2d	|- ( ( C e. Cat /\ S e. V ) -> ( Homf ` D ) = ( Homf ` ( C |`s ( S i^i ( Base ` C ) ) ) ) )
17		eqid	|- ( Homf ` C ) = ( Homf ` C )
18		simpl	|- ( ( C e. Cat /\ S e. V ) -> C e. Cat )
19		inss2	|- ( S i^i ( Base ` C ) ) C_ ( Base ` C )
20	19	a1i	|- ( ( C e. Cat /\ S e. V ) -> ( S i^i ( Base ` C ) ) C_ ( Base ` C ) )
21		eqid	|- ( C |`s ( S i^i ( Base ` C ) ) ) = ( C |`s ( S i^i ( Base ` C ) ) )
22		eqid	|- ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) = ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) )
23	12 17 18 20 21 22	fullresc	|- ( ( C e. Cat /\ S e. V ) -> ( ( Homf ` ( C |`s ( S i^i ( Base ` C ) ) ) ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) /\ ( comf ` ( C |`s ( S i^i ( Base ` C ) ) ) ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) ) )
24	23	simpld	|- ( ( C e. Cat /\ S e. V ) -> ( Homf ` ( C |`s ( S i^i ( Base ` C ) ) ) ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) )
25	16 24	eqtrd	|- ( ( C e. Cat /\ S e. V ) -> ( Homf ` D ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) )
26	15	fveq2d	|- ( ( C e. Cat /\ S e. V ) -> ( comf ` D ) = ( comf ` ( C |`s ( S i^i ( Base ` C ) ) ) ) )
27	23	simprd	|- ( ( C e. Cat /\ S e. V ) -> ( comf ` ( C |`s ( S i^i ( Base ` C ) ) ) ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) )
28	26 27	eqtrd	|- ( ( C e. Cat /\ S e. V ) -> ( comf ` D ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) )
29	1	ovexi	|- D e. _V
30	29	a1i	|- ( ( C e. Cat /\ S e. V ) -> D e. _V )
31		ovexd	|- ( ( C e. Cat /\ S e. V ) -> ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) e. _V )
32	10 11 25 28 30 30 30 31	funcpropd	|- ( ( C e. Cat /\ S e. V ) -> ( D Func D ) = ( D Func ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) )
33	12 17 18 20	fullsubc	|- ( ( C e. Cat /\ S e. V ) -> ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) e. ( Subcat ` C ) )
34		funcres2	|- ( ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) e. ( Subcat ` C ) -> ( D Func ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) C_ ( D Func C ) )
35	33 34	syl	|- ( ( C e. Cat /\ S e. V ) -> ( D Func ( C |`cat ( ( Homf ` C ) |` ( ( S i^i ( Base ` C ) ) X. ( S i^i ( Base ` C ) ) ) ) ) ) C_ ( D Func C ) )
36	32 35	eqsstrd	|- ( ( C e. Cat /\ S e. V ) -> ( D Func D ) C_ ( D Func C ) )
37	36 7	sseldd	|- ( ( C e. Cat /\ S e. V ) -> I e. ( D Func C ) )
38	9 37	eqeltrrd	|- ( ( C e. Cat /\ S e. V ) -> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( D Func C ) )
39		df-br	|- ( ( 1st ` I ) ( D Func C ) ( 2nd ` I ) <-> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( D Func C ) )
40	38 39	sylibr	|- ( ( C e. Cat /\ S e. V ) -> ( 1st ` I ) ( D Func C ) ( 2nd ` I ) )
41		f1oi	|- ( _I |` ( x ( Hom ` D ) y ) ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( x ( Hom ` D ) y )
42		eqid	|- ( Base ` D ) = ( Base ` D )
43	5	adantr	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> D e. Cat )
44		eqid	|- ( Hom ` D ) = ( Hom ` D )
45		simprl	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` D ) )
46		simprr	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) )
47	2 42 43 44 45 46	idfu2nd	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( 2nd ` I ) y ) = ( _I |` ( x ( Hom ` D ) y ) ) )
48		eqidd	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( Hom ` D ) y ) = ( x ( Hom ` D ) y ) )
49		eqid	|- ( Hom ` C ) = ( Hom ` C )
50	1 49	resshom	|- ( S e. V -> ( Hom ` C ) = ( Hom ` D ) )
51	50	ad2antlr	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Hom ` C ) = ( Hom ` D ) )
52	2 42 43 45	idfu1	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( 1st ` I ) ` x ) = x )
53	2 42 43 46	idfu1	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( 1st ` I ) ` y ) = y )
54	51 52 53	oveq123d	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) = ( x ( Hom ` D ) y ) )
55	47 48 54	f1oeq123d	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x ( 2nd ` I ) y ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) <-> ( _I |` ( x ( Hom ` D ) y ) ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( x ( Hom ` D ) y ) ) )
56	41 55	mpbiri	|- ( ( ( C e. Cat /\ S e. V ) /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( 2nd ` I ) y ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) )
57	56	ralrimivva	|- ( ( C e. Cat /\ S e. V ) -> A. x e. ( Base ` D ) A. y e. ( Base ` D ) ( x ( 2nd ` I ) y ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) )
58	42 44 49	isffth2	|- ( ( 1st ` I ) ( ( D Full C ) i^i ( D Faith C ) ) ( 2nd ` I ) <-> ( ( 1st ` I ) ( D Func C ) ( 2nd ` I ) /\ A. x e. ( Base ` D ) A. y e. ( Base ` D ) ( x ( 2nd ` I ) y ) : ( x ( Hom ` D ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) ) )
59	40 57 58	sylanbrc	|- ( ( C e. Cat /\ S e. V ) -> ( 1st ` I ) ( ( D Full C ) i^i ( D Faith C ) ) ( 2nd ` I ) )
60		df-br	|- ( ( 1st ` I ) ( ( D Full C ) i^i ( D Faith C ) ) ( 2nd ` I ) <-> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( ( D Full C ) i^i ( D Faith C ) ) )
61	59 60	sylib	|- ( ( C e. Cat /\ S e. V ) -> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( ( D Full C ) i^i ( D Faith C ) ) )
62	9 61	eqeltrd	|- ( ( C e. Cat /\ S e. V ) -> I e. ( ( D Full C ) i^i ( D Faith C ) ) )