Theorem 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	⊢ ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( Homf ‘ ( SetCat ‘ 1o ) ) ∈ V
2		1oex	⊢ 1o ∈ V
3		eqid	⊢ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ }
4		eqid	⊢ ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) = ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) )
5		eqid	⊢ ( SetCat ‘ 1o ) = ( SetCat ‘ 1o )
6		eqid	⊢ ( Homf ‘ ( SetCat ‘ 1o ) ) = ( Homf ‘ ( SetCat ‘ 1o ) )
7		eqid	⊢ 1o = 1o
8		eqid	⊢ ( Homf ‘ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ) = ( Homf ‘ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } )
9		eqid	⊢ ( Id ‘ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ) = ( Id ‘ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } )
10		eqid	⊢ ( { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ↾cat ( Homf ‘ ( SetCat ‘ 1o ) ) ) = ( { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ↾cat ( Homf ‘ ( SetCat ‘ 1o ) ) )
11	3 4 5 6 7 8 9 10	setc1onsubc	⊢ ( { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ∈ Cat ∧ ( Homf ‘ ( SetCat ‘ 1o ) ) Fn ( 1o × 1o ) ∧ ( ( Homf ‘ ( SetCat ‘ 1o ) ) ⊆cat ( Homf ‘ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ) ∧ ¬ ∀ 𝑥 ∈ 1o ( ( Id ‘ { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ) ‘ 𝑥 ) ∈ ( 𝑥 ( Homf ‘ ( SetCat ‘ 1o ) ) 𝑥 ) ∧ ( { ⟨ ( Base ‘ ndx ) , { ∅ } ⟩ , ⟨ ( Hom ‘ ndx ) , { ⟨ ∅ , ∅ , 2o ⟩ } ⟩ , ⟨ ( comp ‘ ndx ) , { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , ( 𝑓 ∈ 2o , 𝑔 ∈ 2o ↦ ( 𝑓 ∩ 𝑔 ) ) ⟩ } ⟩ } ↾cat ( Homf ‘ ( SetCat ‘ 1o ) ) ) ∈ Cat ) )
12	1 2 11	cnelsubclem	⊢ ∃ 𝑐 ∈ Cat ∃ 𝑗 ∃ 𝑠 ( 𝑗 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑗 ⊆cat ( Homf ‘ 𝑐 ) ∧ ¬ ∀ 𝑥 ∈ 𝑠 ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑗 𝑥 ) ∧ ( 𝑐 ↾cat 𝑗 ) ∈ Cat ) )