Metamath Proof Explorer

Theorem issubc3

Description: Alternate definition of a subcategory, as a subset of the category which is itself a category. The assumption that the identity be closed is necessary just as in the case of a monoid, issubm2 , for the same reasons, since categories are a generalization of monoids. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses issubc3.h 
|- H = ( Homf ` C )
issubc3.i 
|- .1. = ( Id ` C )
issubc3.1 
|- D = ( C |`cat J )
issubc3.c 
|- ( ph -> C e. Cat )
issubc3.a 
|- ( ph -> J Fn ( S X. S ) )
Assertion issubc3 
|- ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) )

Proof

Step Hyp Ref Expression
1 issubc3.h 
 |-  H = ( Homf ` C )
2 issubc3.i 
 |-  .1. = ( Id ` C )
3 issubc3.1 
 |-  D = ( C |`cat J )
4 issubc3.c 
 |-  ( ph -> C e. Cat )
5 issubc3.a 
 |-  ( ph -> J Fn ( S X. S ) )
6 simpr 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> J e. ( Subcat ` C ) )
7 6 1 subcssc 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> J C_cat H )
8 6 adantr 
 |-  ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> J e. ( Subcat ` C ) )
9 5 ad2antrr 
 |-  ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> J Fn ( S X. S ) )
10 simpr 
 |-  ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> x e. S )
11 8 9 10 2 subcidcl 
 |-  ( ( ( ph /\ J e. ( Subcat ` C ) ) /\ x e. S ) -> ( .1. ` x ) e. ( x J x ) )
12 11 ralrimiva 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> A. x e. S ( .1. ` x ) e. ( x J x ) )
13 3 6 subccat 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> D e. Cat )
14 7 12 13 3jca 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) )
15 simpr1 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> J C_cat H )
16 simpr2 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> A. x e. S ( .1. ` x ) e. ( x J x ) )
17 eqid 
 |-  ( Base ` D ) = ( Base ` D )
18 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
19 eqid 
 |-  ( comp ` D ) = ( comp ` D )
20 simplrr 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> D e. Cat )
21 simprl1 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> x e. S )
22 eqid 
 |-  ( Base ` C ) = ( Base ` C )
23 4 ad2antrr 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> C e. Cat )
24 5 ad2antrr 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> J Fn ( S X. S ) )
25 1 22 homffn 
 |-  H Fn ( ( Base ` C ) X. ( Base ` C ) )
26 25 a1i 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> H Fn ( ( Base ` C ) X. ( Base ` C ) ) )
27 simplrl 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> J C_cat H )
28 24 26 27 ssc1 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> S C_ ( Base ` C ) )
29 3 22 23 24 28 rescbas 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> S = ( Base ` D ) )
30 21 29 eleqtrd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> x e. ( Base ` D ) )
31 simprl2 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> y e. S )
32 31 29 eleqtrd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> y e. ( Base ` D ) )
33 simprl3 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> z e. S )
34 33 29 eleqtrd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> z e. ( Base ` D ) )
35 simprrl 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> f e. ( x J y ) )
36 3 22 23 24 28 reschom 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> J = ( Hom ` D ) )
37 36 oveqd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( x J y ) = ( x ( Hom ` D ) y ) )
38 35 37 eleqtrd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> f e. ( x ( Hom ` D ) y ) )
39 simprrr 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> g e. ( y J z ) )
40 36 oveqd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( y J z ) = ( y ( Hom ` D ) z ) )
41 39 40 eleqtrd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> g e. ( y ( Hom ` D ) z ) )
42 17 18 19 20 30 32 34 38 41 catcocl 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( g ( <. x , y >. ( comp ` D ) z ) f ) e. ( x ( Hom ` D ) z ) )
43 eqid 
 |-  ( comp ` C ) = ( comp ` C )
44 3 22 23 24 28 43 rescco 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( comp ` C ) = ( comp ` D ) )
45 44 oveqd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( <. x , y >. ( comp ` C ) z ) = ( <. x , y >. ( comp ` D ) z ) )
46 45 oveqd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
47 36 oveqd 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( x J z ) = ( x ( Hom ` D ) z ) )
48 42 46 47 3eltr4d 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) )
49 48 anassrs 
 |-  ( ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) )
50 49 ralrimivva 
 |-  ( ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) /\ ( x e. S /\ y e. S /\ z e. S ) ) -> A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) )
51 50 ralrimivvva 
 |-  ( ( ph /\ ( J C_cat H /\ D e. Cat ) ) -> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) )
52 51 3adantr2 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) )
53 r19.26 
 |-  ( A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) <-> ( A. x e. S ( .1. ` x ) e. ( x J x ) /\ A. x e. S A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
54 16 52 53 sylanbrc 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) )
55 4 adantr 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> C e. Cat )
56 5 adantr 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> J Fn ( S X. S ) )
57 1 2 43 55 56 issubc2 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> ( J e. ( Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
58 15 54 57 mpbir2and 
 |-  ( ( ph /\ ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) -> J e. ( Subcat ` C ) )
59 14 58 impbida 
 |-  ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat H /\ A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) ) )