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 ) )