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

Metamath Proof Explorer

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 eqtrid 
 |-  ( ( 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 ) ) )