Metamath Proof Explorer

Theorem ssccatid

Description: A category C restricted by J is a category if all of the following are satisfied: a) the base is a subset of base of C , b) all hom-sets are subsets of hom-sets of C , c) it has identity morphisms for all objects, d) the composition under C is closed in J . But J might not be a subcategory of C (see cnelsubc ). (Contributed by Zhi Wang, 6-Nov-2025)

Ref Expression
Hypotheses ssccatid.h 
|- H = ( Homf ` C )
ssccatid.d 
|- D = ( C |`cat J )
ssccatid.x 
|- .x. = ( comp ` C )
ssccatid.j 
|- ( ph -> J C_cat H )
ssccatid.f 
|- ( ph -> J Fn ( S X. S ) )
ssccatid.c 
|- ( ph -> C e. Cat )
ssccatid.i 
|- ( ( ph /\ y e. S ) -> .1. e. ( y J y ) )
ssccatid.l 
|- ( ( ph /\ ( a e. S /\ b e. S /\ m e. ( a J b ) ) ) -> ( .1. ( <. a , b >. .x. b ) m ) = m )
ssccatid.r 
|- ( ( ph /\ ( a e. S /\ b e. S /\ m e. ( a J b ) ) ) -> ( m ( <. a , a >. .x. b ) .1. ) = m )
ssccatid.1 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) )
Assertion ssccatid 
|- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( y e. S |-> .1. ) ) )

Proof

Step Hyp Ref Expression
1 ssccatid.h 
 |-  H = ( Homf ` C )
2 ssccatid.d 
 |-  D = ( C |`cat J )
3 ssccatid.x 
 |-  .x. = ( comp ` C )
4 ssccatid.j 
 |-  ( ph -> J C_cat H )
5 ssccatid.f 
 |-  ( ph -> J Fn ( S X. S ) )
6 ssccatid.c 
 |-  ( ph -> C e. Cat )
7 ssccatid.i 
 |-  ( ( ph /\ y e. S ) -> .1. e. ( y J y ) )
8 ssccatid.l 
 |-  ( ( ph /\ ( a e. S /\ b e. S /\ m e. ( a J b ) ) ) -> ( .1. ( <. a , b >. .x. b ) m ) = m )
9 ssccatid.r 
 |-  ( ( ph /\ ( a e. S /\ b e. S /\ m e. ( a J b ) ) ) -> ( m ( <. a , a >. .x. b ) .1. ) = m )
10 ssccatid.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 1 11 homffn 
 |-  H Fn ( ( Base ` C ) X. ( Base ` C ) )
13 12 a1i 
 |-  ( ph -> H Fn ( ( Base ` C ) X. ( Base ` C ) ) )
14 5 13 4 ssc1 
 |-  ( ph -> S C_ ( Base ` C ) )
15 2 11 6 5 14 rescbas 
 |-  ( ph -> S = ( Base ` D ) )
16 2 11 6 5 14 reschom 
 |-  ( ph -> J = ( Hom ` D ) )
17 2 11 6 5 14 3 rescco 
 |-  ( ph -> .x. = ( comp ` D ) )
18 2 ovexi 
 |-  D e. _V
19 18 a1i 
 |-  ( ph -> D e. _V )
20 biid 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) <-> ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) )
21 oveq2 
 |-  ( m = f -> ( .1. ( <. x , y >. .x. y ) m ) = ( .1. ( <. x , y >. .x. y ) f ) )
22 id 
 |-  ( m = f -> m = f )
23 21 22 eqeq12d 
 |-  ( m = f -> ( ( .1. ( <. x , y >. .x. y ) m ) = m <-> ( .1. ( <. x , y >. .x. y ) f ) = f ) )
24 oveq1 
 |-  ( a = x -> ( a J b ) = ( x J b ) )
25 opeq1 
 |-  ( a = x -> <. a , b >. = <. x , b >. )
26 25 oveq1d 
 |-  ( a = x -> ( <. a , b >. .x. b ) = ( <. x , b >. .x. b ) )
27 26 oveqd 
 |-  ( a = x -> ( .1. ( <. a , b >. .x. b ) m ) = ( .1. ( <. x , b >. .x. b ) m ) )
28 27 eqeq1d 
 |-  ( a = x -> ( ( .1. ( <. a , b >. .x. b ) m ) = m <-> ( .1. ( <. x , b >. .x. b ) m ) = m ) )
29 24 28 raleqbidv 
 |-  ( a = x -> ( A. m e. ( a J b ) ( .1. ( <. a , b >. .x. b ) m ) = m <-> A. m e. ( x J b ) ( .1. ( <. x , b >. .x. b ) m ) = m ) )
30 oveq2 
 |-  ( b = y -> ( x J b ) = ( x J y ) )
31 opeq2 
 |-  ( b = y -> <. x , b >. = <. x , y >. )
32 id 
 |-  ( b = y -> b = y )
33 31 32 oveq12d 
 |-  ( b = y -> ( <. x , b >. .x. b ) = ( <. x , y >. .x. y ) )
34 33 oveqd 
 |-  ( b = y -> ( .1. ( <. x , b >. .x. b ) m ) = ( .1. ( <. x , y >. .x. y ) m ) )
35 34 eqeq1d 
 |-  ( b = y -> ( ( .1. ( <. x , b >. .x. b ) m ) = m <-> ( .1. ( <. x , y >. .x. y ) m ) = m ) )
36 30 35 raleqbidv 
 |-  ( b = y -> ( A. m e. ( x J b ) ( .1. ( <. x , b >. .x. b ) m ) = m <-> A. m e. ( x J y ) ( .1. ( <. x , y >. .x. y ) m ) = m ) )
37 8 ralrimivvva 
 |-  ( ph -> A. a e. S A. b e. S A. m e. ( a J b ) ( .1. ( <. a , b >. .x. b ) m ) = m )
38 37 adantr 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> A. a e. S A. b e. S A. m e. ( a J b ) ( .1. ( <. a , b >. .x. b ) m ) = m )
39 simpr1l 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> x e. S )
40 simpr1r 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> y e. S )
41 29 36 38 39 40 rspc2dv 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> A. m e. ( x J y ) ( .1. ( <. x , y >. .x. y ) m ) = m )
42 simpr31 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> f e. ( x J y ) )
43 23 41 42 rspcdva 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
44 oveq1 
 |-  ( m = g -> ( m ( <. y , y >. .x. z ) .1. ) = ( g ( <. y , y >. .x. z ) .1. ) )
45 id 
 |-  ( m = g -> m = g )
46 44 45 eqeq12d 
 |-  ( m = g -> ( ( m ( <. y , y >. .x. z ) .1. ) = m <-> ( g ( <. y , y >. .x. z ) .1. ) = g ) )
47 oveq1 
 |-  ( a = y -> ( a J b ) = ( y J b ) )
48 id 
 |-  ( a = y -> a = y )
49 48 48 opeq12d 
 |-  ( a = y -> <. a , a >. = <. y , y >. )
50 49 oveq1d 
 |-  ( a = y -> ( <. a , a >. .x. b ) = ( <. y , y >. .x. b ) )
51 50 oveqd 
 |-  ( a = y -> ( m ( <. a , a >. .x. b ) .1. ) = ( m ( <. y , y >. .x. b ) .1. ) )
52 51 eqeq1d 
 |-  ( a = y -> ( ( m ( <. a , a >. .x. b ) .1. ) = m <-> ( m ( <. y , y >. .x. b ) .1. ) = m ) )
53 47 52 raleqbidv 
 |-  ( a = y -> ( A. m e. ( a J b ) ( m ( <. a , a >. .x. b ) .1. ) = m <-> A. m e. ( y J b ) ( m ( <. y , y >. .x. b ) .1. ) = m ) )
54 oveq2 
 |-  ( b = z -> ( y J b ) = ( y J z ) )
55 oveq2 
 |-  ( b = z -> ( <. y , y >. .x. b ) = ( <. y , y >. .x. z ) )
56 55 oveqd 
 |-  ( b = z -> ( m ( <. y , y >. .x. b ) .1. ) = ( m ( <. y , y >. .x. z ) .1. ) )
57 56 eqeq1d 
 |-  ( b = z -> ( ( m ( <. y , y >. .x. b ) .1. ) = m <-> ( m ( <. y , y >. .x. z ) .1. ) = m ) )
58 54 57 raleqbidv 
 |-  ( b = z -> ( A. m e. ( y J b ) ( m ( <. y , y >. .x. b ) .1. ) = m <-> A. m e. ( y J z ) ( m ( <. y , y >. .x. z ) .1. ) = m ) )
59 9 ralrimivvva 
 |-  ( ph -> A. a e. S A. b e. S A. m e. ( a J b ) ( m ( <. a , a >. .x. b ) .1. ) = m )
60 59 adantr 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> A. a e. S A. b e. S A. m e. ( a J b ) ( m ( <. a , a >. .x. b ) .1. ) = m )
61 simpr2l 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> z e. S )
62 53 58 60 40 61 rspc2dv 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> A. m e. ( y J z ) ( m ( <. y , y >. .x. z ) .1. ) = m )
63 simpr32 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> g e. ( y J z ) )
64 46 62 63 rspcdva 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
65 simpl 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ph )
66 65 39 40 61 42 63 10 syl132anc 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x J z ) )
67 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
68 6 adantr 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> C e. Cat )
69 14 adantr 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> S C_ ( Base ` C ) )
70 69 39 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> x e. ( Base ` C ) )
71 69 40 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> y e. ( Base ` C ) )
72 69 61 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> z e. ( Base ` C ) )
73 5 adantr 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> J Fn ( S X. S ) )
74 4 adantr 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> J C_cat H )
75 73 74 39 40 ssc2 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( x J y ) C_ ( x H y ) )
76 75 42 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> f e. ( x H y ) )
77 1 11 67 70 71 homfval 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( x H y ) = ( x ( Hom ` C ) y ) )
78 76 77 eleqtrd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> f e. ( x ( Hom ` C ) y ) )
79 73 74 40 61 ssc2 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( y J z ) C_ ( y H z ) )
80 79 63 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> g e. ( y H z ) )
81 1 11 67 71 72 homfval 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( y H z ) = ( y ( Hom ` C ) z ) )
82 80 81 eleqtrd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> g e. ( y ( Hom ` C ) z ) )
83 simpr2r 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> w e. S )
84 69 83 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> w e. ( Base ` C ) )
85 73 74 61 83 ssc2 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( z J w ) C_ ( z H w ) )
86 simpr33 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> k e. ( z J w ) )
87 85 86 sseldd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> k e. ( z H w ) )
88 1 11 67 72 84 homfval 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( z H w ) = ( z ( Hom ` C ) w ) )
89 87 88 eleqtrd 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> k e. ( z ( Hom ` C ) w ) )
90 11 67 3 68 70 71 72 78 82 84 89 catass 
 |-  ( ( ph /\ ( ( x e. S /\ y e. S ) /\ ( z e. S /\ w e. S ) /\ ( f e. ( x J y ) /\ g e. ( y J z ) /\ k e. ( z J w ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
91 15 16 17 19 20 7 43 64 66 90 iscatd2 
 |-  ( ph -> ( D e. Cat /\ ( Id ` D ) = ( y e. S |-> .1. ) ) )