Metamath Proof Explorer

Theorem idffth

Description: The identity functor is a fully faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypothesis idffth.i 
|- I = ( idFunc ` C )
Assertion idffth 
|- ( C e. Cat -> I e. ( ( C Full C ) i^i ( C Faith C ) ) )

Proof

Step Hyp Ref Expression
1 idffth.i 
 |-  I = ( idFunc ` C )
2 relfunc 
 |-  Rel ( C Func C )
3 1 idfucl 
 |-  ( C e. Cat -> I e. ( C Func C ) )
4 1st2nd 
 |-  ( ( Rel ( C Func C ) /\ I e. ( C Func C ) ) -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
5 2 3 4 sylancr 
 |-  ( C e. Cat -> I = <. ( 1st ` I ) , ( 2nd ` I ) >. )
6 5 3 eqeltrrd 
 |-  ( C e. Cat -> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( C Func C ) )
7 df-br 
 |-  ( ( 1st ` I ) ( C Func C ) ( 2nd ` I ) <-> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( C Func C ) )
8 6 7 sylibr 
 |-  ( C e. Cat -> ( 1st ` I ) ( C Func C ) ( 2nd ` I ) )
9 f1oi 
 |-  ( _I |` ( x ( Hom ` C ) y ) ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( x ( Hom ` C ) y )
10 eqid 
 |-  ( Base ` C ) = ( Base ` C )
11 simpl 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. Cat )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 simprl 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
14 simprr 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
15 1 10 11 12 13 14 idfu2nd 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` I ) y ) = ( _I |` ( x ( Hom ` C ) y ) ) )
16 eqidd 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` C ) y ) )
17 1 10 11 13 idfu1 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` I ) ` x ) = x )
18 1 10 11 14 idfu1 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( 1st ` I ) ` y ) = y )
19 17 18 oveq12d 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) = ( x ( Hom ` C ) y ) )
20 15 16 19 f1oeq123d 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( x ( 2nd ` I ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) <-> ( _I |` ( x ( Hom ` C ) y ) ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( x ( Hom ` C ) y ) ) )
21 9 20 mpbiri 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` I ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) )
22 21 ralrimivva 
 |-  ( C e. Cat -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( 2nd ` I ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) )
23 10 12 12 isffth2 
 |-  ( ( 1st ` I ) ( ( C Full C ) i^i ( C Faith C ) ) ( 2nd ` I ) <-> ( ( 1st ` I ) ( C Func C ) ( 2nd ` I ) /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( 2nd ` I ) y ) : ( x ( Hom ` C ) y ) -1-1-onto-> ( ( ( 1st ` I ) ` x ) ( Hom ` C ) ( ( 1st ` I ) ` y ) ) ) )
24 8 22 23 sylanbrc 
 |-  ( C e. Cat -> ( 1st ` I ) ( ( C Full C ) i^i ( C Faith C ) ) ( 2nd ` I ) )
25 df-br 
 |-  ( ( 1st ` I ) ( ( C Full C ) i^i ( C Faith C ) ) ( 2nd ` I ) <-> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( ( C Full C ) i^i ( C Faith C ) ) )
26 24 25 sylib 
 |-  ( C e. Cat -> <. ( 1st ` I ) , ( 2nd ` I ) >. e. ( ( C Full C ) i^i ( C Faith C ) ) )
27 5 26 eqeltrd 
 |-  ( C e. Cat -> I e. ( ( C Full C ) i^i ( C Faith C ) ) )