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	⊢ 𝐵 = ( Base ‘ 𝐶 )
	nelsubc.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	nelsubc.0	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
	nelsubc.j	⊢ ( 𝜑 → 𝐽 = ( ( 𝑆 × 𝑆 ) × { ∅ } ) )
	nelsubc.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
	nelsubc.i	⊢ 1 = ( Id ‘ 𝐶 )
	nelsubc.o	⊢ · = ( comp ‘ 𝐶 )
Assertion	nelsubc	⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nelsubc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		nelsubc.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
3		nelsubc.0	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
4		nelsubc.j	⊢ ( 𝜑 → 𝐽 = ( ( 𝑆 × 𝑆 ) × { ∅ } ) )
5		nelsubc.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
6		nelsubc.i	⊢ 1 = ( Id ‘ 𝐶 )
7		nelsubc.o	⊢ · = ( comp ‘ 𝐶 )
8	1 2 3 4 5	nelsubclem	⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ · 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )