Theorem nelsubc

Description: An empty "hom-set" for non-empty base satisfies all conditions for a subcategory but the existence of identity morphisms. (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. { (/) } ) )
	nelsubc.h	|- H = ( Homf ` C )
	nelsubc.i	|- .1. = ( Id ` C )
	nelsubc.o	|- .x. = ( comp ` C )
Assertion	nelsubc	|- ( ph -> ( J Fn ( S X. S ) /\ ( J C_cat H /\ ( -. 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 >. .x. z ) f ) e. ( x J z ) ) ) ) )

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		nelsubc.h	|- H = ( Homf ` C )
6		nelsubc.i	|- .1. = ( Id ` C )
7		nelsubc.o	|- .x. = ( comp ` C )
8	1 2 3 4 5	nelsubclem	|- ( ph -> ( J Fn ( S X. S ) /\ ( J C_cat H /\ ( -. 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 >. .x. z ) f ) e. ( x J z ) ) ) ) )