cnelsubc

Description: Remark 4.2(2) of Adamek p. 48. There exists acategory satisfying all conditions for a subcategory but the compatibility of identity morphisms. Therefore such condition in df-subc is necessary. A stronger statement than nelsubc3 . (Contributed by Zhi Wang, 6-Nov-2025)

		Ref	Expression
	Assertion	cnelsubc	$⊢ \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 c ↾_{cat} j \in Cat))$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ {Hom}_{𝑓} (SetCat (1_{𝑜})) \in V$
2		1oex	$⊢ 1_{𝑜} \in V$
3		eqid	$⊢ \{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\} = \{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\}$
4		eqid	$⊢ (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g) = (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)$
5		eqid	$⊢ SetCat (1_{𝑜}) = SetCat (1_{𝑜})$
6		eqid	$⊢ {Hom}_{𝑓} (SetCat (1_{𝑜})) = {Hom}_{𝑓} (SetCat (1_{𝑜}))$
7		eqid	$⊢ 1_{𝑜} = 1_{𝑜}$
8		eqid	$⊢ {Hom}_{𝑓} (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\}) = {Hom}_{𝑓} (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\})$
9		eqid	$⊢ Id (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\}) = Id (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\})$
10		eqid	$⊢ \{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\} ↾_{cat} {Hom}_{𝑓} (SetCat (1_{𝑜})) = \{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\} ↾_{cat} {Hom}_{𝑓} (SetCat (1_{𝑜}))$
11	3 4 5 6 7 8 9 10	setc1onsubc	$⊢ (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\} \in Cat \land {Hom}_{𝑓} (SetCat (1_{𝑜})) Fn (1_{𝑜} \times 1_{𝑜}) \land ({Hom}_{𝑓} (SetCat (1_{𝑜})) \subseteq_{cat} {Hom}_{𝑓} (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\}) \land \neg \forall x \in 1_{𝑜} Id (\{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\}) (x) \in (x {Hom}_{𝑓} (SetCat (1_{𝑜})) x) \land \{⟨{Base}_{ndx}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)⟩\}⟩\} ↾_{cat} {Hom}_{𝑓} (SetCat (1_{𝑜})) \in Cat))$
12	1 2 11	cnelsubclem	$⊢ \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 c ↾_{cat} j \in Cat))$

Metamath Proof Explorer

Theorem cnelsubc

Proof