Theorem 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	⊢ ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2oex	⊢ 2o ∈ V
2		eqid	⊢ ( SetCat ‘ 2o ) = ( SetCat ‘ 2o )
3	2	setccat	⊢ ( 2o ∈ V → ( SetCat ‘ 2o ) ∈ Cat )
4	1 3	ax-mp	⊢ ( SetCat ‘ 2o ) ∈ Cat
5		1oex	⊢ 1o ∈ V
6	5 5	xpex	⊢ ( 1o × 1o ) ∈ V
7		p0ex	⊢ { ∅ } ∈ V
8	6 7	xpex	⊢ ( ( 1o × 1o ) × { ∅ } ) ∈ V
9	1	a1i	⊢ ( ⊤ → 2o ∈ V )
10	2 9	setcbas	⊢ ( ⊤ → 2o = ( Base ‘ ( SetCat ‘ 2o ) ) )
11	10	mptru	⊢ 2o = ( Base ‘ ( SetCat ‘ 2o ) )
12		2on0	⊢ 2o ≠ ∅
13		2on	⊢ 2o ∈ On
14	13	onordi	⊢ Ord 2o
15		ordge1n0	⊢ ( Ord 2o → ( 1o ⊆ 2o ↔ 2o ≠ ∅ ) )
16	14 15	ax-mp	⊢ ( 1o ⊆ 2o ↔ 2o ≠ ∅ )
17	12 16	mpbir	⊢ 1o ⊆ 2o
18	17	a1i	⊢ ( ⊤ → 1o ⊆ 2o )
19		1n0	⊢ 1o ≠ ∅
20	19	a1i	⊢ ( ⊤ → 1o ≠ ∅ )
21		eqidd	⊢ ( ⊤ → ( ( 1o × 1o ) × { ∅ } ) = ( ( 1o × 1o ) × { ∅ } ) )
22		eqid	⊢ ( Homf ‘ ( SetCat ‘ 2o ) ) = ( Homf ‘ ( SetCat ‘ 2o ) )
23	11 18 20 21 22	nelsubclem	⊢ ( ⊤ → ( ( ( 1o × 1o ) × { ∅ } ) Fn ( 1o × 1o ) ∧ ( ( ( 1o × 1o ) × { ∅ } ) ⊆cat ( Homf ‘ ( SetCat ‘ 2o ) ) ∧ ( ¬ ∀ 𝑥 ∈ 1o ( ( Id ‘ ( SetCat ‘ 2o ) ) ‘ 𝑥 ) ∈ ( 𝑥 ( ( 1o × 1o ) × { ∅ } ) 𝑥 ) ∧ ∀ 𝑥 ∈ 1o ∀ 𝑦 ∈ 1o ∀ 𝑧 ∈ 1o ∀ 𝑓 ∈ ( 𝑥 ( ( 1o × 1o ) × { ∅ } ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( ( 1o × 1o ) × { ∅ } ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( SetCat ‘ 2o ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 1o × 1o ) × { ∅ } ) 𝑧 ) ) ) ) )
24	23	mptru	⊢ ( ( ( 1o × 1o ) × { ∅ } ) Fn ( 1o × 1o ) ∧ ( ( ( 1o × 1o ) × { ∅ } ) ⊆cat ( Homf ‘ ( SetCat ‘ 2o ) ) ∧ ( ¬ ∀ 𝑥 ∈ 1o ( ( Id ‘ ( SetCat ‘ 2o ) ) ‘ 𝑥 ) ∈ ( 𝑥 ( ( 1o × 1o ) × { ∅ } ) 𝑥 ) ∧ ∀ 𝑥 ∈ 1o ∀ 𝑦 ∈ 1o ∀ 𝑧 ∈ 1o ∀ 𝑓 ∈ ( 𝑥 ( ( 1o × 1o ) × { ∅ } ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( ( 1o × 1o ) × { ∅ } ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( SetCat ‘ 2o ) ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 1o × 1o ) × { ∅ } ) 𝑧 ) ) ) )
25	4 8 5 24	nelsubc3lem	⊢ ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ∀ 𝑧 ∈ 𝑠 ∀ 𝑓 ∈ ( 𝑥 𝑗 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑗 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑗 𝑧 ) ) ) )