Metamath Proof Explorer

Theorem fthfunc

Description: A faithful functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Assertion fthfunc 
|- ( C Faith D ) C_ ( C Func D )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( c = C -> ( c Faith d ) = ( C Faith d ) )
2 oveq1 
 |-  ( c = C -> ( c Func d ) = ( C Func d ) )
3 1 2 sseq12d 
 |-  ( c = C -> ( ( c Faith d ) C_ ( c Func d ) <-> ( C Faith d ) C_ ( C Func d ) ) )
4 oveq2 
 |-  ( d = D -> ( C Faith d ) = ( C Faith D ) )
5 oveq2 
 |-  ( d = D -> ( C Func d ) = ( C Func D ) )
6 4 5 sseq12d 
 |-  ( d = D -> ( ( C Faith d ) C_ ( C Func d ) <-> ( C Faith D ) C_ ( C Func D ) ) )
7 ovex 
 |-  ( c Func d ) e. _V
8 simpl 
 |-  ( ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) -> f ( c Func d ) g )
9 8 ssopab2i 
 |-  { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } C_ { <. f , g >. | f ( c Func d ) g }
10 opabss 
 |-  { <. f , g >. | f ( c Func d ) g } C_ ( c Func d )
11 9 10 sstri 
 |-  { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } C_ ( c Func d )
12 7 11 ssexi 
 |-  { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } e. _V
13 df-fth 
 |-  Faith = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )
14 13 ovmpt4g 
 |-  ( ( c e. Cat /\ d e. Cat /\ { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } e. _V ) -> ( c Faith d ) = { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )
15 12 14 mp3an3 
 |-  ( ( c e. Cat /\ d e. Cat ) -> ( c Faith d ) = { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )
16 15 11 eqsstrdi 
 |-  ( ( c e. Cat /\ d e. Cat ) -> ( c Faith d ) C_ ( c Func d ) )
17 3 6 16 vtocl2ga 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) C_ ( C Func D ) )
18 13 mpondm0 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) = (/) )
19 0ss 
 |-  (/) C_ ( C Func D )
20 18 19 eqsstrdi 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) C_ ( C Func D ) )
21 17 20 pm2.61i 
 |-  ( C Faith D ) C_ ( C Func D )