nelsubc3

Description: Remark 4.2(2) of Adamek p. 48. There exists a set satisfying all conditions for a subcategory but the existence of identity morphisms. Therefore such condition in df-subc is necessary.

Note that this theorem cheated a little bit because ` ( C |``cat J ) ` is not a category. In fact ` ( C |``cat J ) e. Cat ` is a stronger statement than the condition (d) of Definition 4.1(1) of Adamek p. 48, as stated here (see the proof of issubc3 ). To construct such a category, see setc1onsubc and cnelsubc . (Contributed by Zhi Wang, 5-Nov-2025)

		Ref	Expression
	Assertion	nelsubc3	$⊢ \exists c \in Cat \exists j \exists s (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))))$

Proof

Step	Hyp	Ref	Expression
1		2oex	$⊢ 2_{𝑜} \in V$
2		eqid	$⊢ SetCat (2_{𝑜}) = SetCat (2_{𝑜})$
3	2	setccat	$⊢ 2_{𝑜} \in V \to SetCat (2_{𝑜}) \in Cat$
4	1 3	ax-mp	$⊢ SetCat (2_{𝑜}) \in Cat$
5		1oex	$⊢ 1_{𝑜} \in V$
6	5 5	xpex	$⊢ 1_{𝑜} \times 1_{𝑜} \in V$
7		p0ex	$⊢ \{\emptyset\} \in V$
8	6 7	xpex	$⊢ (1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\} \in V$
9	1	a1i	$⊢ ⊤ \to 2_{𝑜} \in V$
10	2 9	setcbas	$⊢ ⊤ \to 2_{𝑜} = {Base}_{SetCat (2_{𝑜})}$
11	10	mptru	$⊢ 2_{𝑜} = {Base}_{SetCat (2_{𝑜})}$
12		2on0	$⊢ 2_{𝑜} \neq \emptyset$
13		2on	$⊢ 2_{𝑜} \in On$
14	13	onordi	$⊢ Ord 2_{𝑜}$
15		ordge1n0	$⊢ Ord 2_{𝑜} \to (1_{𝑜} \subseteq 2_{𝑜} \leftrightarrow 2_{𝑜} \neq \emptyset)$
16	14 15	ax-mp	$⊢ 1_{𝑜} \subseteq 2_{𝑜} \leftrightarrow 2_{𝑜} \neq \emptyset$
17	12 16	mpbir	$⊢ 1_{𝑜} \subseteq 2_{𝑜}$
18	17	a1i	$⊢ ⊤ \to 1_{𝑜} \subseteq 2_{𝑜}$
19		1n0	$⊢ 1_{𝑜} \neq \emptyset$
20	19	a1i	$⊢ ⊤ \to 1_{𝑜} \neq \emptyset$
21		eqidd	$⊢ ⊤ \to (1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\} = (1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}$
22		eqid	$⊢ {Hom}_{𝑓} (SetCat (2_{𝑜})) = {Hom}_{𝑓} (SetCat (2_{𝑜}))$
23	11 18 20 21 22	nelsubclem	$⊢ ⊤ \to (((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) Fn (1_{𝑜} \times 1_{𝑜}) \land (((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) \subseteq_{cat} {Hom}_{𝑓} (SetCat (2_{𝑜})) \land (\neg \forall x \in 1_{𝑜} Id (SetCat (2_{𝑜})) (x) \in (x ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) x) \land \forall x \in 1_{𝑜} \forall y \in 1_{𝑜} \forall z \in 1_{𝑜} \forall f \in (x ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) y) \forall g \in (y ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) z) g (⟨x, y⟩ comp (SetCat (2_{𝑜})) z) f \in (x ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) z))))$
24	23	mptru	$⊢ (((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) Fn (1_{𝑜} \times 1_{𝑜}) \land (((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) \subseteq_{cat} {Hom}_{𝑓} (SetCat (2_{𝑜})) \land (\neg \forall x \in 1_{𝑜} Id (SetCat (2_{𝑜})) (x) \in (x ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) x) \land \forall x \in 1_{𝑜} \forall y \in 1_{𝑜} \forall z \in 1_{𝑜} \forall f \in (x ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) y) \forall g \in (y ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) z) g (⟨x, y⟩ comp (SetCat (2_{𝑜})) z) f \in (x ((1_{𝑜} \times 1_{𝑜}) \times \{\emptyset\}) z))))$
25	4 8 5 24	nelsubc3lem	$⊢ \exists c \in Cat \exists j \exists s (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))))$

Metamath Proof Explorer

Theorem nelsubc3

Proof