Metamath Proof Explorer

Theorem nelsubc2

Description: An empty "hom-set" for non-empty base is not a subcategory. (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses nelsubc.b 
|- B = ( Base ` C )
nelsubc.s 
|- ( ph -> S C_ B )
nelsubc.0 
|- ( ph -> S =/= (/) )
nelsubc.j 
|- ( ph -> J = ( ( S X. S ) X. { (/) } ) )
nelsubc2.c 
|- ( ph -> C e. Cat )
Assertion nelsubc2 
|- ( ph -> -. J e. ( Subcat ` C ) )

Proof

Step Hyp Ref Expression
1 nelsubc.b 
 |-  B = ( Base ` C )
2 nelsubc.s 
 |-  ( ph -> S C_ B )
3 nelsubc.0 
 |-  ( ph -> S =/= (/) )
4 nelsubc.j 
 |-  ( ph -> J = ( ( S X. S ) X. { (/) } ) )
5 nelsubc2.c 
 |-  ( ph -> C e. Cat )
6 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
7 eqid 
 |-  ( Id ` C ) = ( Id ` C )
8 eqid 
 |-  ( comp ` C ) = ( comp ` C )
9 1 2 3 4 6 7 8 nelsubc 
 |-  ( ph -> ( J Fn ( S X. S ) /\ ( J C_cat ( Homf ` C ) /\ ( -. A. x e. S ( ( Id ` C ) ` 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 ) ) ) ) )
10 9 simprrd 
 |-  ( ph -> ( -. A. x e. S ( ( Id ` C ) ` 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 ) ) )
11 10 simpld 
 |-  ( ph -> -. A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) )
12 9 simpld 
 |-  ( ph -> J Fn ( S X. S ) )
13 6 7 8 5 12 issubc2 
 |-  ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( ( Id ` C ) ` 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 ) ) ) ) )
14 13 simplbda 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> A. x e. S ( ( ( Id ` C ) ` 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 ) ) )
15 r19.26 
 |-  ( A. x e. S ( ( ( Id ` C ) ` 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 ( ( Id ` C ) ` 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 ) ) )
16 14 15 sylib 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> ( A. x e. S ( ( Id ` C ) ` 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 ) ) )
17 16 simpld 
 |-  ( ( ph /\ J e. ( Subcat ` C ) ) -> A. x e. S ( ( Id ` C ) ` x ) e. ( x J x ) )
18 11 17 mtand 
 |-  ( ph -> -. J e. ( Subcat ` C ) )