Metamath Proof Explorer

Theorem subccatid

Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subccat.1 
|- D = ( C |`cat J )
subccat.j 
|- ( ph -> J e. ( Subcat ` C ) )
subccatid.1 
|- ( ph -> J Fn ( S X. S ) )
subccatid.2 
|- .1. = ( Id ` C )
Assertion subccatid 
|- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 subccat.1 
 |-  D = ( C |`cat J )
2 subccat.j 
 |-  ( ph -> J e. ( Subcat ` C ) )
3 subccatid.1 
 |-  ( ph -> J Fn ( S X. S ) )
4 subccatid.2 
 |-  .1. = ( Id ` C )
5 eqid 
 |-  ( Base ` C ) = ( Base ` C )
6 subcrcl 
 |-  ( J e. ( Subcat ` C ) -> C e. Cat )
7 2 6 syl 
 |-  ( ph -> C e. Cat )
8 2 3 5 subcss1 
 |-  ( ph -> S C_ ( Base ` C ) )
9 1 5 7 3 8 rescbas 
 |-  ( ph -> S = ( Base ` D ) )
10 1 5 7 3 8 reschom 
 |-  ( ph -> J = ( Hom ` D ) )
11 eqid 
 |-  ( comp ` C ) = ( comp ` C )
12 1 5 7 3 8 11 rescco 
 |-  ( ph -> ( comp ` C ) = ( comp ` D ) )
13 1 ovexi 
 |-  D e. _V
14 13 a1i 
 |-  ( ph -> D e. _V )
15 biid 
 |-  ( ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) <-> ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) )
16 2 adantr 
 |-  ( ( ph /\ x e. S ) -> J e. ( Subcat ` C ) )
17 3 adantr 
 |-  ( ( ph /\ x e. S ) -> J Fn ( S X. S ) )
18 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
19 16 17 18 4 subcidcl 
 |-  ( ( ph /\ x e. S ) -> ( .1. ` x ) e. ( x J x ) )
20 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
21 7 adantr 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> C e. Cat )
22 8 adantr 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> S C_ ( Base ` C ) )
23 simpr1l 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> w e. S )
24 22 23 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> w e. ( Base ` C ) )
25 simpr1r 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> x e. S )
26 22 25 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> x e. ( Base ` C ) )
27 2 adantr 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> J e. ( Subcat ` C ) )
28 3 adantr 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> J Fn ( S X. S ) )
29 27 28 20 23 25 subcss2 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( w J x ) C_ ( w ( Hom ` C ) x ) )
30 simpr31 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> f e. ( w J x ) )
31 29 30 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> f e. ( w ( Hom ` C ) x ) )
32 5 20 4 21 24 11 26 31 catlid 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( ( .1. ` x ) ( <. w , x >. ( comp ` C ) x ) f ) = f )
33 simpr2l 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> y e. S )
34 22 33 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> y e. ( Base ` C ) )
35 27 28 20 25 33 subcss2 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( x J y ) C_ ( x ( Hom ` C ) y ) )
36 simpr32 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> g e. ( x J y ) )
37 35 36 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> g e. ( x ( Hom ` C ) y ) )
38 5 20 4 21 26 11 34 37 catrid 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( .1. ` x ) ) = g )
39 27 28 23 11 25 33 30 36 subccocl 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( g ( <. w , x >. ( comp ` C ) y ) f ) e. ( w J y ) )
40 simpr2r 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> z e. S )
41 22 40 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> z e. ( Base ` C ) )
42 27 28 20 33 40 subcss2 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( y J z ) C_ ( y ( Hom ` C ) z ) )
43 simpr33 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> h e. ( y J z ) )
44 42 43 sseldd 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> h e. ( y ( Hom ` C ) z ) )
45 5 20 11 21 24 26 34 31 37 41 44 catass 
 |-  ( ( ph /\ ( ( w e. S /\ x e. S ) /\ ( y e. S /\ z e. S ) /\ ( f e. ( w J x ) /\ g e. ( x J y ) /\ h e. ( y J z ) ) ) ) -> ( ( h ( <. x , y >. ( comp ` C ) z ) g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g ( <. w , x >. ( comp ` C ) y ) f ) ) )
46 9 10 12 14 15 19 32 38 39 45 iscatd2 
 |-  ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) )