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 )