Metamath Proof Explorer

Theorem discsubc

Description: A discrete category, whose only morphisms are the identity morphisms, is a subcategory. (Contributed by Zhi Wang, 1-Nov-2025)

Ref Expression
Hypotheses discsubc.j 
|- J = ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) )
discsubc.b 
|- B = ( Base ` C )
discsubc.i 
|- I = ( Id ` C )
discsubc.s 
|- ( ph -> S C_ B )
discsubc.c 
|- ( ph -> C e. Cat )
Assertion discsubc 
|- ( ph -> J e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 discsubc.j 
 |-  J = ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) )
2 discsubc.b 
 |-  B = ( Base ` C )
3 discsubc.i 
 |-  I = ( Id ` C )
4 discsubc.s 
 |-  ( ph -> S C_ B )
5 discsubc.c 
 |-  ( ph -> C e. Cat )
6 eqeq12 
 |-  ( ( x = a /\ y = b ) -> ( x = y <-> a = b ) )
7 simpl 
 |-  ( ( x = a /\ y = b ) -> x = a )
8 7 fveq2d 
 |-  ( ( x = a /\ y = b ) -> ( I ` x ) = ( I ` a ) )
9 8 sneqd 
 |-  ( ( x = a /\ y = b ) -> { ( I ` x ) } = { ( I ` a ) } )
10 6 9 ifbieq1d 
 |-  ( ( x = a /\ y = b ) -> if ( x = y , { ( I ` x ) } , (/) ) = if ( a = b , { ( I ` a ) } , (/) ) )
11 snex 
 |-  { ( I ` a ) } e. _V
12 0ex 
 |-  (/) e. _V
13 11 12 ifex 
 |-  if ( a = b , { ( I ` a ) } , (/) ) e. _V
14 10 1 13 ovmpoa 
 |-  ( ( a e. S /\ b e. S ) -> ( a J b ) = if ( a = b , { ( I ` a ) } , (/) ) )
15 14 adantl 
 |-  ( ( ph /\ ( a e. S /\ b e. S ) ) -> ( a J b ) = if ( a = b , { ( I ` a ) } , (/) ) )
16 sseq1 
 |-  ( { ( I ` a ) } = if ( a = b , { ( I ` a ) } , (/) ) -> ( { ( I ` a ) } C_ ( a ( Homf ` C ) b ) <-> if ( a = b , { ( I ` a ) } , (/) ) C_ ( a ( Homf ` C ) b ) ) )
17 sseq1 
 |-  ( (/) = if ( a = b , { ( I ` a ) } , (/) ) -> ( (/) C_ ( a ( Homf ` C ) b ) <-> if ( a = b , { ( I ` a ) } , (/) ) C_ ( a ( Homf ` C ) b ) ) )
18 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
19 5 ad2antrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> C e. Cat )
20 4 ad2antrr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> S C_ B )
21 simplrl 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> a e. S )
22 20 21 sseldd 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> a e. B )
23 2 18 3 19 22 catidcl 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> ( I ` a ) e. ( a ( Hom ` C ) a ) )
24 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
25 24 2 18 22 22 homfval 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> ( a ( Homf ` C ) a ) = ( a ( Hom ` C ) a ) )
26 simpr 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> a = b )
27 26 oveq2d 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> ( a ( Homf ` C ) a ) = ( a ( Homf ` C ) b ) )
28 25 27 eqtr3d 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> ( a ( Hom ` C ) a ) = ( a ( Homf ` C ) b ) )
29 23 28 eleqtrd 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> ( I ` a ) e. ( a ( Homf ` C ) b ) )
30 29 snssd 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ a = b ) -> { ( I ` a ) } C_ ( a ( Homf ` C ) b ) )
31 0ss 
 |-  (/) C_ ( a ( Homf ` C ) b )
32 31 a1i 
 |-  ( ( ( ph /\ ( a e. S /\ b e. S ) ) /\ -. a = b ) -> (/) C_ ( a ( Homf ` C ) b ) )
33 16 17 30 32 ifbothda 
 |-  ( ( ph /\ ( a e. S /\ b e. S ) ) -> if ( a = b , { ( I ` a ) } , (/) ) C_ ( a ( Homf ` C ) b ) )
34 15 33 eqsstrd 
 |-  ( ( ph /\ ( a e. S /\ b e. S ) ) -> ( a J b ) C_ ( a ( Homf ` C ) b ) )
35 34 ralrimivva 
 |-  ( ph -> A. a e. S A. b e. S ( a J b ) C_ ( a ( Homf ` C ) b ) )
36 1 discsubclem 
 |-  J Fn ( S X. S )
37 36 a1i 
 |-  ( ph -> J Fn ( S X. S ) )
38 24 2 homffn 
 |-  ( Homf ` C ) Fn ( B X. B )
39 38 a1i 
 |-  ( ph -> ( Homf ` C ) Fn ( B X. B ) )
40 2 fvexi 
 |-  B e. _V
41 40 a1i 
 |-  ( ph -> B e. _V )
42 37 39 41 isssc 
 |-  ( ph -> ( J C_cat ( Homf ` C ) <-> ( S C_ B /\ A. a e. S A. b e. S ( a J b ) C_ ( a ( Homf ` C ) b ) ) ) )
43 4 35 42 mpbir2and 
 |-  ( ph -> J C_cat ( Homf ` C ) )
44 fvex 
 |-  ( I ` a ) e. _V
45 44 snid 
 |-  ( I ` a ) e. { ( I ` a ) }
46 simpr 
 |-  ( ( ph /\ a e. S ) -> a e. S )
47 equtr2 
 |-  ( ( x = a /\ y = a ) -> x = y )
48 47 iftrued 
 |-  ( ( x = a /\ y = a ) -> if ( x = y , { ( I ` x ) } , (/) ) = { ( I ` x ) } )
49 simpl 
 |-  ( ( x = a /\ y = a ) -> x = a )
50 49 fveq2d 
 |-  ( ( x = a /\ y = a ) -> ( I ` x ) = ( I ` a ) )
51 50 sneqd 
 |-  ( ( x = a /\ y = a ) -> { ( I ` x ) } = { ( I ` a ) } )
52 48 51 eqtrd 
 |-  ( ( x = a /\ y = a ) -> if ( x = y , { ( I ` x ) } , (/) ) = { ( I ` a ) } )
53 52 1 11 ovmpoa 
 |-  ( ( a e. S /\ a e. S ) -> ( a J a ) = { ( I ` a ) } )
54 46 46 53 syl2anc 
 |-  ( ( ph /\ a e. S ) -> ( a J a ) = { ( I ` a ) } )
55 45 54 eleqtrrid 
 |-  ( ( ph /\ a e. S ) -> ( I ` a ) e. ( a J a ) )
56 45 a1i 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( I ` a ) e. { ( I ` a ) } )
57 simprl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> f e. ( a J b ) )
58 46 ad2antrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> a e. S )
59 simplrl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> b e. S )
60 58 59 14 syl2anc 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( a J b ) = if ( a = b , { ( I ` a ) } , (/) ) )
61 57 60 eleqtrd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> f e. if ( a = b , { ( I ` a ) } , (/) ) )
62 61 ne0d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> if ( a = b , { ( I ` a ) } , (/) ) =/= (/) )
63 iffalse 
 |-  ( -. a = b -> if ( a = b , { ( I ` a ) } , (/) ) = (/) )
64 63 necon1ai 
 |-  ( if ( a = b , { ( I ` a ) } , (/) ) =/= (/) -> a = b )
65 62 64 syl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> a = b )
66 65 opeq2d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> <. a , a >. = <. a , b >. )
67 simprr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> g e. ( b J c ) )
68 eqeq12 
 |-  ( ( x = b /\ y = c ) -> ( x = y <-> b = c ) )
69 simpl 
 |-  ( ( x = b /\ y = c ) -> x = b )
70 69 fveq2d 
 |-  ( ( x = b /\ y = c ) -> ( I ` x ) = ( I ` b ) )
71 70 sneqd 
 |-  ( ( x = b /\ y = c ) -> { ( I ` x ) } = { ( I ` b ) } )
72 68 71 ifbieq1d 
 |-  ( ( x = b /\ y = c ) -> if ( x = y , { ( I ` x ) } , (/) ) = if ( b = c , { ( I ` b ) } , (/) ) )
73 snex 
 |-  { ( I ` b ) } e. _V
74 73 12 ifex 
 |-  if ( b = c , { ( I ` b ) } , (/) ) e. _V
75 72 1 74 ovmpoa 
 |-  ( ( b e. S /\ c e. S ) -> ( b J c ) = if ( b = c , { ( I ` b ) } , (/) ) )
76 75 ad2antlr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( b J c ) = if ( b = c , { ( I ` b ) } , (/) ) )
77 67 76 eleqtrd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> g e. if ( b = c , { ( I ` b ) } , (/) ) )
78 77 ne0d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> if ( b = c , { ( I ` b ) } , (/) ) =/= (/) )
79 iffalse 
 |-  ( -. b = c -> if ( b = c , { ( I ` b ) } , (/) ) = (/) )
80 79 necon1ai 
 |-  ( if ( b = c , { ( I ` b ) } , (/) ) =/= (/) -> b = c )
81 78 80 syl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> b = c )
82 65 81 eqtrd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> a = c )
83 66 82 oveq12d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( <. a , a >. ( comp ` C ) a ) = ( <. a , b >. ( comp ` C ) c ) )
84 83 eqcomd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( <. a , b >. ( comp ` C ) c ) = ( <. a , a >. ( comp ` C ) a ) )
85 81 iftrued 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> if ( b = c , { ( I ` b ) } , (/) ) = { ( I ` b ) } )
86 77 85 eleqtrd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> g e. { ( I ` b ) } )
87 86 elsnd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> g = ( I ` b ) )
88 65 fveq2d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( I ` a ) = ( I ` b ) )
89 87 88 eqtr4d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> g = ( I ` a ) )
90 65 iftrued 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> if ( a = b , { ( I ` a ) } , (/) ) = { ( I ` a ) } )
91 61 90 eleqtrd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> f e. { ( I ` a ) } )
92 91 elsnd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> f = ( I ` a ) )
93 84 89 92 oveq123d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) = ( ( I ` a ) ( <. a , a >. ( comp ` C ) a ) ( I ` a ) ) )
94 5 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> C e. Cat )
95 4 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> S C_ B )
96 95 58 sseldd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> a e. B )
97 eqid 
 |-  ( comp ` C ) = ( comp ` C )
98 2 18 3 94 96 catidcl 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( I ` a ) e. ( a ( Hom ` C ) a ) )
99 2 18 3 94 96 97 96 98 catlid 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( ( I ` a ) ( <. a , a >. ( comp ` C ) a ) ( I ` a ) ) = ( I ` a ) )
100 93 99 eqtrd 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) = ( I ` a ) )
101 82 oveq2d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( a J a ) = ( a J c ) )
102 58 58 53 syl2anc 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( a J a ) = { ( I ` a ) } )
103 101 102 eqtr3d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( a J c ) = { ( I ` a ) } )
104 56 100 103 3eltr4d 
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) /\ ( f e. ( a J b ) /\ g e. ( b J c ) ) ) -> ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a J c ) )
105 104 ralrimivva 
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. S /\ c e. S ) ) -> A. f e. ( a J b ) A. g e. ( b J c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a J c ) )
106 105 ralrimivva 
 |-  ( ( ph /\ a e. S ) -> A. b e. S A. c e. S A. f e. ( a J b ) A. g e. ( b J c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a J c ) )
107 55 106 jca 
 |-  ( ( ph /\ a e. S ) -> ( ( I ` a ) e. ( a J a ) /\ A. b e. S A. c e. S A. f e. ( a J b ) A. g e. ( b J c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a J c ) ) )
108 107 ralrimiva 
 |-  ( ph -> A. a e. S ( ( I ` a ) e. ( a J a ) /\ A. b e. S A. c e. S A. f e. ( a J b ) A. g e. ( b J c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a J c ) ) )
109 24 3 97 5 37 issubc2 
 |-  ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. a e. S ( ( I ` a ) e. ( a J a ) /\ A. b e. S A. c e. S A. f e. ( a J b ) A. g e. ( b J c ) ( g ( <. a , b >. ( comp ` C ) c ) f ) e. ( a J c ) ) ) ) )
110 43 108 109 mpbir2and 
 |-  ( ph -> J e. ( Subcat ` C ) )