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	$⊢ φ \to S \subseteq B$
		nelsubc.0	$⊢ φ \to S \neq \emptyset$
		nelsubc.j	$⊢ φ \to J = (S \times S) \times \{\emptyset\}$
		nelsubc2.c	$⊢ φ \to C \in Cat$
	Assertion	nelsubc2	$⊢ φ \to \neg J \in Subcat (C)$

Proof

Step	Hyp	Ref	Expression
1		nelsubc.b	$⊢ B = {Base}_{C}$
2		nelsubc.s	$⊢ φ \to S \subseteq B$
3		nelsubc.0	$⊢ φ \to S \neq \emptyset$
4		nelsubc.j	$⊢ φ \to J = (S \times S) \times \{\emptyset\}$
5		nelsubc2.c	$⊢ φ \to C \in Cat$
6		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
7		eqid	$⊢ Id (C) = Id (C)$
8		eqid	$⊢ comp (C) = comp (C)$
9	1 2 3 4 6 7 8	nelsubc	$⊢ φ \to (J Fn (S \times S) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land (\neg \forall x \in S Id (C) (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
10	9	simprrd	$⊢ φ \to (\neg \forall x \in S Id (C) (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
11	10	simpld	$⊢ φ \to \neg \forall x \in S Id (C) (x) \in (x J x)$
12	9	simpld	$⊢ φ \to J Fn (S \times S)$
13	6 7 8 5 12	issubc2	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
14	13	simplbda	$⊢ (φ \land J \in Subcat (C)) \to \forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
15		r19.26	$⊢ \forall x \in S (Id (C) (x) \in (x J x) \land \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)) \leftrightarrow (\forall x \in S Id (C) (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
16	14 15	sylib	$⊢ (φ \land J \in Subcat (C)) \to (\forall x \in S Id (C) (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
17	16	simpld	$⊢ (φ \land J \in Subcat (C)) \to \forall x \in S Id (C) (x) \in (x J x)$
18	11 17	mtand	$⊢ φ \to \neg J \in Subcat (C)$