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