Metamath Proof Explorer

Theorem fullsubc

Description: The full subcategory generated by a subset of objects is the category with these objects and the same morphisms as the original. The result is always a subcategory (and it is full, meaning that all morphisms of the original category between objects in the subcategory is also in the subcategory), see definition 4.1(2) of Adamek p. 48. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses fullsubc.b 
|- B = ( Base ` C )
fullsubc.h 
|- H = ( Homf ` C )
fullsubc.c 
|- ( ph -> C e. Cat )
fullsubc.s 
|- ( ph -> S C_ B )
Assertion fullsubc 
|- ( ph -> ( H |` ( S X. S ) ) e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 fullsubc.b 
 |-  B = ( Base ` C )
2 fullsubc.h 
 |-  H = ( Homf ` C )
3 fullsubc.c 
 |-  ( ph -> C e. Cat )
4 fullsubc.s 
 |-  ( ph -> S C_ B )
5 2 1 homffn 
 |-  H Fn ( B X. B )
6 1 fvexi 
 |-  B e. _V
7 sscres 
 |-  ( ( H Fn ( B X. B ) /\ B e. _V ) -> ( H |` ( S X. S ) ) C_cat H )
8 5 6 7 mp2an 
 |-  ( H |` ( S X. S ) ) C_cat H
9 8 a1i 
 |-  ( ph -> ( H |` ( S X. S ) ) C_cat H )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 eqid 
 |-  ( Id ` C ) = ( Id ` C )
12 3 adantr 
 |-  ( ( ph /\ x e. S ) -> C e. Cat )
13 4 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. B )
14 1 10 11 12 13 catidcl 
 |-  ( ( ph /\ x e. S ) -> ( ( Id ` C ) ` x ) e. ( x ( Hom ` C ) x ) )
15 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
16 15 15 ovresd 
 |-  ( ( ph /\ x e. S ) -> ( x ( H |` ( S X. S ) ) x ) = ( x H x ) )
17 2 1 10 13 13 homfval 
 |-  ( ( ph /\ x e. S ) -> ( x H x ) = ( x ( Hom ` C ) x ) )
18 16 17 eqtrd 
 |-  ( ( ph /\ x e. S ) -> ( x ( H |` ( S X. S ) ) x ) = ( x ( Hom ` C ) x ) )
19 14 18 eleqtrrd 
 |-  ( ( ph /\ x e. S ) -> ( ( Id ` C ) ` x ) e. ( x ( H |` ( S X. S ) ) x ) )
20 eqid 
 |-  ( comp ` C ) = ( comp ` C )
21 12 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> C e. Cat )
22 13 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> x e. B )
23 4 adantr 
 |-  ( ( ph /\ x e. S ) -> S C_ B )
24 23 sselda 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> y e. B )
25 24 adantr 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> y e. B )
26 25 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> y e. B )
27 23 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> S C_ B )
28 27 sselda 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> z e. B )
29 28 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> z e. B )
30 simprl 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> f e. ( x ( Hom ` C ) y ) )
31 simprr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> g e. ( y ( Hom ` C ) z ) )
32 1 10 20 21 22 26 29 30 31 catcocl 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
33 15 ad3antrrr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> x e. S )
34 simplr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> z e. S )
35 33 34 ovresd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( H |` ( S X. S ) ) z ) = ( x H z ) )
36 2 1 10 22 29 homfval 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x H z ) = ( x ( Hom ` C ) z ) )
37 35 36 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( H |` ( S X. S ) ) z ) = ( x ( Hom ` C ) z ) )
38 32 37 eleqtrrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) )
39 38 ralrimivva 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) )
40 simplr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> x e. S )
41 simpr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> y e. S )
42 40 41 ovresd 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> ( x ( H |` ( S X. S ) ) y ) = ( x H y ) )
43 13 adantr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> x e. B )
44 2 1 10 43 24 homfval 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> ( x H y ) = ( x ( Hom ` C ) y ) )
45 42 44 eqtrd 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> ( x ( H |` ( S X. S ) ) y ) = ( x ( Hom ` C ) y ) )
46 45 adantr 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> ( x ( H |` ( S X. S ) ) y ) = ( x ( Hom ` C ) y ) )
47 simplr 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> y e. S )
48 simpr 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> z e. S )
49 47 48 ovresd 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> ( y ( H |` ( S X. S ) ) z ) = ( y H z ) )
50 2 1 10 25 28 homfval 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> ( y H z ) = ( y ( Hom ` C ) z ) )
51 49 50 eqtrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> ( y ( H |` ( S X. S ) ) z ) = ( y ( Hom ` C ) z ) )
52 51 raleqdv 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> ( A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) <-> A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) ) )
53 46 52 raleqbidv 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> ( A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) <-> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) ) )
54 39 53 mpbird 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. S ) /\ z e. S ) -> A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) )
55 54 ralrimiva 
 |-  ( ( ( ph /\ x e. S ) /\ y e. S ) -> A. z e. S A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) )
56 55 ralrimiva 
 |-  ( ( ph /\ x e. S ) -> A. y e. S A. z e. S A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) )
57 19 56 jca 
 |-  ( ( ph /\ x e. S ) -> ( ( ( Id ` C ) ` x ) e. ( x ( H |` ( S X. S ) ) x ) /\ A. y e. S A. z e. S A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) ) )
58 57 ralrimiva 
 |-  ( ph -> A. x e. S ( ( ( Id ` C ) ` x ) e. ( x ( H |` ( S X. S ) ) x ) /\ A. y e. S A. z e. S A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) ) )
59 xpss12 
 |-  ( ( S C_ B /\ S C_ B ) -> ( S X. S ) C_ ( B X. B ) )
60 4 4 59 syl2anc 
 |-  ( ph -> ( S X. S ) C_ ( B X. B ) )
61 fnssres 
 |-  ( ( H Fn ( B X. B ) /\ ( S X. S ) C_ ( B X. B ) ) -> ( H |` ( S X. S ) ) Fn ( S X. S ) )
62 5 60 61 sylancr 
 |-  ( ph -> ( H |` ( S X. S ) ) Fn ( S X. S ) )
63 2 11 20 3 62 issubc2 
 |-  ( ph -> ( ( H |` ( S X. S ) ) e. ( Subcat ` C ) <-> ( ( H |` ( S X. S ) ) C_cat H /\ A. x e. S ( ( ( Id ` C ) ` x ) e. ( x ( H |` ( S X. S ) ) x ) /\ A. y e. S A. z e. S A. f e. ( x ( H |` ( S X. S ) ) y ) A. g e. ( y ( H |` ( S X. S ) ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( H |` ( S X. S ) ) z ) ) ) ) )
64 9 58 63 mpbir2and 
 |-  ( ph -> ( H |` ( S X. S ) ) e. ( Subcat ` C ) )