Metamath Proof Explorer

Theorem resssetc

Description: The restriction of the category of sets to a subset is the category of sets in the subset. Thus, the SetCatU categories for different U are full subcategories of each other. (Contributed by Mario Carneiro, 6-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 resssetc 
|- ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) )

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 3 4 ssexd 
 |-  ( ph -> V e. _V )
6 5 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> V e. _V )
7 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
8 simprl 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. V )
9 simprr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. V )
10 2 6 7 8 9 setchom 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x ( Hom ` D ) y ) = ( y ^m x ) )
11 3 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> U e. W )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 4 adantr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> V C_ U )
14 13 8 sseldd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. U )
15 13 9 sseldd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. U )
16 1 11 12 14 15 setchom 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x ( Hom ` C ) y ) = ( y ^m x ) )
17 eqid 
 |-  ( C |`s V ) = ( C |`s V )
18 17 12 resshom 
 |-  ( V e. _V -> ( Hom ` C ) = ( Hom ` ( C |`s V ) ) )
19 5 18 syl 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` ( C |`s V ) ) )
20 19 oveqdr 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` ( C |`s V ) ) y ) )
21 10 16 20 3eqtr2rd 
 |-  ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( x ( Hom ` ( C |`s V ) ) y ) = ( x ( Hom ` D ) y ) )
22 21 ralrimivva 
 |-  ( ph -> A. x e. V A. y e. V ( x ( Hom ` ( C |`s V ) ) y ) = ( x ( Hom ` D ) y ) )
23 eqid 
 |-  ( Hom ` ( C |`s V ) ) = ( Hom ` ( C |`s V ) )
24 1 3 setcbas 
 |-  ( ph -> U = ( Base ` C ) )
25 4 24 sseqtrd 
 |-  ( ph -> V C_ ( Base ` C ) )
26 eqid 
 |-  ( Base ` C ) = ( Base ` C )
27 17 26 ressbas2 
 |-  ( V C_ ( Base ` C ) -> V = ( Base ` ( C |`s V ) ) )
28 25 27 syl 
 |-  ( ph -> V = ( Base ` ( C |`s V ) ) )
29 2 5 setcbas 
 |-  ( ph -> V = ( Base ` D ) )
30 23 7 28 29 homfeq 
 |-  ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) <-> A. x e. V A. y e. V ( x ( Hom ` ( C |`s V ) ) y ) = ( x ( Hom ` D ) y ) ) )
31 22 30 mpbird 
 |-  ( ph -> ( Homf ` ( C |`s V ) ) = ( Homf ` D ) )
32 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> V e. _V )
33 eqid 
 |-  ( comp ` D ) = ( comp ` D )
34 simplr1 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> x e. V )
35 simplr2 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> y e. V )
36 simplr3 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> z e. V )
37 simprl 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> f e. ( x ( Hom ` D ) y ) )
38 2 32 7 34 35 elsetchom 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( f e. ( x ( Hom ` D ) y ) <-> f : x --> y ) )
39 37 38 mpbid 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> f : x --> y )
40 simprr 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> g e. ( y ( Hom ` D ) z ) )
41 2 32 7 35 36 elsetchom 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g e. ( y ( Hom ` D ) z ) <-> g : y --> z ) )
42 40 41 mpbid 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> g : y --> z )
43 2 32 33 34 35 36 39 42 setcco 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g o. f ) )
44 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> U e. W )
45 eqid 
 |-  ( comp ` C ) = ( comp ` C )
46 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> V C_ U )
47 46 34 sseldd 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> x e. U )
48 46 35 sseldd 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> y e. U )
49 46 36 sseldd 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> z e. U )
50 1 44 45 47 48 49 39 42 setcco 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g o. f ) )
51 17 45 ressco 
 |-  ( V e. _V -> ( comp ` C ) = ( comp ` ( C |`s V ) ) )
52 5 51 syl 
 |-  ( ph -> ( comp ` C ) = ( comp ` ( C |`s V ) ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( comp ` C ) = ( comp ` ( C |`s V ) ) )
54 53 oveqd 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( <. x , y >. ( comp ` C ) z ) = ( <. x , y >. ( comp ` ( C |`s V ) ) z ) )
55 54 oveqd 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
56 43 50 55 3eqtr2d 
 |-  ( ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) /\ ( f e. ( x ( Hom ` D ) y ) /\ g e. ( y ( Hom ` D ) z ) ) ) -> ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
57 56 ralrimivva 
 |-  ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
58 57 ralrimivvva 
 |-  ( ph -> A. x e. V A. y e. V A. z e. V A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) )
59 eqid 
 |-  ( comp ` ( C |`s V ) ) = ( comp ` ( C |`s V ) )
60 31 eqcomd 
 |-  ( ph -> ( Homf ` D ) = ( Homf ` ( C |`s V ) ) )
61 33 59 7 29 28 60 comfeq 
 |-  ( ph -> ( ( comf ` D ) = ( comf ` ( C |`s V ) ) <-> A. x e. V A. y e. V A. z e. V A. f e. ( x ( Hom ` D ) y ) A. g e. ( y ( Hom ` D ) z ) ( g ( <. x , y >. ( comp ` D ) z ) f ) = ( g ( <. x , y >. ( comp ` ( C |`s V ) ) z ) f ) ) )
62 58 61 mpbird 
 |-  ( ph -> ( comf ` D ) = ( comf ` ( C |`s V ) ) )
63 62 eqcomd 
 |-  ( ph -> ( comf ` ( C |`s V ) ) = ( comf ` D ) )
64 31 63 jca 
 |-  ( ph -> ( ( Homf ` ( C |`s V ) ) = ( Homf ` D ) /\ ( comf ` ( C |`s V ) ) = ( comf ` D ) ) )