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={\mathrm{Base}}_C$$
	nelsubc.s	$$⊢\phi \to S\subseteq B$$
	nelsubc.0	$$⊢\phi \to S\ne \varnothing$$
	nelsubc.j	$$⊢\phi \to J=\left(S\times S\right)\times \left\{\varnothing \right\}$$
	nelsubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(C\right)$$
	nelsubc.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	nelsubc.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
Assertion	nelsubc	$$⊢\phi \to \left(JFn\left(S\times S\right)\wedge \left(J{\subseteq }_{\mathrm{cat}}H\wedge \left(\neg \forall x\in S\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\wedge \forall x\in S\forall y\in S\forall z\in S\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f\in \left(xJz\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nelsubc.b	$$⊢B={\mathrm{Base}}_C$$
2		nelsubc.s	$$⊢\phi \to S\subseteq B$$
3		nelsubc.0	$$⊢\phi \to S\ne \varnothing$$
4		nelsubc.j	$$⊢\phi \to J=\left(S\times S\right)\times \left\{\varnothing \right\}$$
5		nelsubc.h	$$⊢H={\mathrm{Hom}}_{𝑓}\left(C\right)$$
6		nelsubc.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
7		nelsubc.o	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(C\right)$$
8	1 2 3 4 5	nelsubclem	$$⊢\phi \to \left(JFn\left(S\times S\right)\wedge \left(J{\subseteq }_{\mathrm{cat}}H\wedge \left(\neg \forall x\in S\underset{\dot{}}{1}\left(x\right)\in \left(xJx\right)\wedge \forall x\in S\forall y\in S\forall z\in S\forall f\in \left(xJy\right)\forall g\in \left(yJz\right)g\left(⟨x,y⟩\underset{\dot{}}{·}z\right)f\in \left(xJz\right)\right)\right)\right)$$