Metamath Proof Explorer

Theorem funcsetcres2

Description: A functor into a smaller category of sets is a functor into the larger category. (Contributed by Mario Carneiro, 28-Jan-2017)

Ref Expression
Hypotheses resssetc.c 
|- C = ( SetCat ` U )
resssetc.d 
|- D = ( SetCat ` V )
resssetc.1 
|- ( ph -> U e. W )
resssetc.2 
|- ( ph -> V C_ U )
Assertion funcsetcres2 
|- ( ph -> ( E Func D ) C_ ( E Func C ) )

Proof

Step Hyp Ref Expression
1 resssetc.c 
 |-  C = ( SetCat ` U )
2 resssetc.d 
 |-  D = ( SetCat ` V )
3 resssetc.1 
 |-  ( ph -> U e. W )
4 resssetc.2 
 |-  ( ph -> V C_ U )
5 eqidd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` E ) = ( Homf ` E ) )
6 eqidd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` E ) = ( comf ` E ) )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
9 1 setccat 
 |-  ( U e. W -> C e. Cat )
10 3 9 syl 
 |-  ( ph -> C e. Cat )
11 10 adantr 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> C e. Cat )
12 1 3 setcbas 
 |-  ( ph -> U = ( Base ` C ) )
13 4 12 sseqtrd 
 |-  ( ph -> V C_ ( Base ` C ) )
14 13 adantr 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> V C_ ( Base ` C ) )
15 eqid 
 |-  ( C |`s V ) = ( C |`s V )
16 eqid 
 |-  ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) = ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) )
17 7 8 11 14 15 16 fullresc 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) /\ ( comf ` ( C |`s V ) ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) ) )
18 17 simpld 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` ( C |`s V ) ) = ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) )
19 1 2 3 4 resssetc 
 |-  ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) )
20 19 adantr 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) )
21 20 simpld 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` ( C |`s V ) ) = ( Homf ` D ) )
22 18 21 eqtr3d 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( Homf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) = ( Homf ` D ) )
23 17 simprd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` ( C |`s V ) ) = ( comf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) )
24 20 simprd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` ( C |`s V ) ) = ( comf ` D ) )
25 23 24 eqtr3d 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( comf ` ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) = ( comf ` D ) )
26 funcrcl 
 |-  ( f e. ( E Func D ) -> ( E e. Cat /\ D e. Cat ) )
27 26 adantl 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( E e. Cat /\ D e. Cat ) )
28 27 simpld 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> E e. Cat )
29 7 8 11 14 fullsubc 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( ( Homf ` C ) |` ( V X. V ) ) e. ( Subcat ` C ) )
30 16 29 subccat 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) e. Cat )
31 27 simprd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> D e. Cat )
32 5 6 22 25 28 28 30 31 funcpropd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( E Func ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) = ( E Func D ) )
33 funcres2 
 |-  ( ( ( Homf ` C ) |` ( V X. V ) ) e. ( Subcat ` C ) -> ( E Func ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) C_ ( E Func C ) )
34 29 33 syl 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( E Func ( C |`cat ( ( Homf ` C ) |` ( V X. V ) ) ) ) C_ ( E Func C ) )
35 32 34 eqsstrrd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> ( E Func D ) C_ ( E Func C ) )
36 simpr 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> f e. ( E Func D ) )
37 35 36 sseldd 
 |-  ( ( ph /\ f e. ( E Func D ) ) -> f e. ( E Func C ) )
38 37 ex 
 |-  ( ph -> ( f e. ( E Func D ) -> f e. ( E Func C ) ) )
39 38 ssrdv 
 |-  ( ph -> ( E Func D ) C_ ( E Func C ) )