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	|- E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ ( -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2oex	|- 2o e. _V
2		eqid	|- ( SetCat ` 2o ) = ( SetCat ` 2o )
3	2	setccat	|- ( 2o e. _V -> ( SetCat ` 2o ) e. Cat )
4	1 3	ax-mp	|- ( SetCat ` 2o ) e. Cat
5		1oex	|- 1o e. _V
6	5 5	xpex	|- ( 1o X. 1o ) e. _V
7		p0ex	|- { (/) } e. _V
8	6 7	xpex	|- ( ( 1o X. 1o ) X. { (/) } ) e. _V
9	1	a1i	|- ( T. -> 2o e. _V )
10	2 9	setcbas	|- ( T. -> 2o = ( Base ` ( SetCat ` 2o ) ) )
11	10	mptru	|- 2o = ( Base ` ( SetCat ` 2o ) )
12		2on0	|- 2o =/= (/)
13		2on	|- 2o e. On
14	13	onordi	|- Ord 2o
15		ordge1n0	|- ( Ord 2o -> ( 1o C_ 2o <-> 2o =/= (/) ) )
16	14 15	ax-mp	|- ( 1o C_ 2o <-> 2o =/= (/) )
17	12 16	mpbir	|- 1o C_ 2o
18	17	a1i	|- ( T. -> 1o C_ 2o )
19		1n0	|- 1o =/= (/)
20	19	a1i	|- ( T. -> 1o =/= (/) )
21		eqidd	|- ( T. -> ( ( 1o X. 1o ) X. { (/) } ) = ( ( 1o X. 1o ) X. { (/) } ) )
22		eqid	|- ( Homf ` ( SetCat ` 2o ) ) = ( Homf ` ( SetCat ` 2o ) )
23	11 18 20 21 22	nelsubclem	|- ( T. -> ( ( ( 1o X. 1o ) X. { (/) } ) Fn ( 1o X. 1o ) /\ ( ( ( 1o X. 1o ) X. { (/) } ) C_cat ( Homf ` ( SetCat ` 2o ) ) /\ ( -. A. x e. 1o ( ( Id ` ( SetCat ` 2o ) ) ` x ) e. ( x ( ( 1o X. 1o ) X. { (/) } ) x ) /\ A. x e. 1o A. y e. 1o A. z e. 1o A. f e. ( x ( ( 1o X. 1o ) X. { (/) } ) y ) A. g e. ( y ( ( 1o X. 1o ) X. { (/) } ) z ) ( g ( <. x , y >. ( comp ` ( SetCat ` 2o ) ) z ) f ) e. ( x ( ( 1o X. 1o ) X. { (/) } ) z ) ) ) ) )
24	23	mptru	|- ( ( ( 1o X. 1o ) X. { (/) } ) Fn ( 1o X. 1o ) /\ ( ( ( 1o X. 1o ) X. { (/) } ) C_cat ( Homf ` ( SetCat ` 2o ) ) /\ ( -. A. x e. 1o ( ( Id ` ( SetCat ` 2o ) ) ` x ) e. ( x ( ( 1o X. 1o ) X. { (/) } ) x ) /\ A. x e. 1o A. y e. 1o A. z e. 1o A. f e. ( x ( ( 1o X. 1o ) X. { (/) } ) y ) A. g e. ( y ( ( 1o X. 1o ) X. { (/) } ) z ) ( g ( <. x , y >. ( comp ` ( SetCat ` 2o ) ) z ) f ) e. ( x ( ( 1o X. 1o ) X. { (/) } ) z ) ) ) )
25	4 8 5 24	nelsubc3lem	|- E. c e. Cat E. j E. s ( j Fn ( s X. s ) /\ ( j C_cat ( Homf ` c ) /\ ( -. A. x e. s ( ( Id ` c ) ` x ) e. ( x j x ) /\ A. x e. s A. y e. s A. z e. s A. f e. ( x j y ) A. g e. ( y j z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x j z ) ) ) )