Metamath Proof Explorer

Theorem fullfunc

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

Ref Expression
Assertion fullfunc 
|- ( C Full D ) C_ ( C Func D )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( c = C -> ( c Full d ) = ( C Full d ) )
2 oveq1 
 |-  ( c = C -> ( c Func d ) = ( C Func d ) )
3 1 2 sseq12d 
 |-  ( c = C -> ( ( c Full d ) C_ ( c Func d ) <-> ( C Full d ) C_ ( C Func d ) ) )
4 oveq2 
 |-  ( d = D -> ( C Full d ) = ( C Full D ) )
5 oveq2 
 |-  ( d = D -> ( C Func d ) = ( C Func D ) )
6 4 5 sseq12d 
 |-  ( d = D -> ( ( C Full d ) C_ ( C Func d ) <-> ( C Full 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 ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` 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 ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` 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 ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` 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 ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } e. _V
13 df-full 
 |-  Full = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` 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 ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } e. _V ) -> ( c Full d ) = { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )
15 12 14 mp3an3 
 |-  ( ( c e. Cat /\ d e. Cat ) -> ( c Full d ) = { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )
16 15 11 eqsstrdi 
 |-  ( ( c e. Cat /\ d e. Cat ) -> ( c Full d ) C_ ( c Func d ) )
17 3 6 16 vtocl2ga 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Full D ) C_ ( C Func D ) )
18 13 mpondm0 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Full D ) = (/) )
19 0ss 
 |-  (/) C_ ( C Func D )
20 18 19 eqsstrdi 
 |-  ( -. ( C e. Cat /\ D e. Cat ) -> ( C Full D ) C_ ( C Func D ) )
21 17 20 pm2.61i 
 |-  ( C Full D ) C_ ( C Func D )