Theorem setc1onsubc

Description: Construct a category with one object and two morphisms and prove that category ( SetCat1o ) satisfies all conditions for a subcategory but the compatibility of identity morphisms, showing the necessity of the latter condition in defining a subcategory. Exercise 4A of Adamek p. 58. (Contributed by Zhi Wang, 6-Nov-2025)

	Ref	Expression
Hypotheses	setc1onsubc.c	|- C = { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , .x. >. } >. }
	setc1onsubc.x	|- .x. = ( f e. 2o , g e. 2o |-> ( f i^i g ) )
	setc1onsubc.e	|- E = ( SetCat ` 1o )
	setc1onsubc.j	|- J = ( Homf ` E )
	setc1onsubc.s	|- S = 1o
	setc1onsubc.h	|- H = ( Homf ` C )
	setc1onsubc.i	|- .1. = ( Id ` C )
	setc1onsubc.d	|- D = ( C |`cat J )
Assertion	setc1onsubc	|- ( C e. Cat /\ J Fn ( S X. S ) /\ ( J C_cat H /\ -. A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) )

Proof

Step	Hyp	Ref	Expression
1		setc1onsubc.c	|- C = { <. ( Base ` ndx ) , { (/) } >. , <. ( Hom ` ndx ) , { <. (/) , (/) , 2o >. } >. , <. ( comp ` ndx ) , { <. <. (/) , (/) >. , (/) , .x. >. } >. }
2		setc1onsubc.x	|- .x. = ( f e. 2o , g e. 2o |-> ( f i^i g ) )
3		setc1onsubc.e	|- E = ( SetCat ` 1o )
4		setc1onsubc.j	|- J = ( Homf ` E )
5		setc1onsubc.s	|- S = 1o
6		setc1onsubc.h	|- H = ( Homf ` C )
7		setc1onsubc.i	|- .1. = ( Id ` C )
8		setc1onsubc.d	|- D = ( C |`cat J )
9		0ss	|- (/) C_ 1o
10		1oex	|- 1o e. _V
11		df2o3	|- 2o = { (/) , 1o }
12	1 11 2	incat	|- ( ( (/) C_ 1o /\ 1o e. _V ) -> ( C e. Cat /\ ( Id ` C ) = ( y e. { (/) } |-> 1o ) ) )
13	9 10 12	mp2an	|- ( C e. Cat /\ ( Id ` C ) = ( y e. { (/) } |-> 1o ) )
14	13	simpli	|- C e. Cat
15	3	setc1obas	|- 1o = ( Base ` E )
16	5 15	eqtri	|- S = ( Base ` E )
17	4 16	homffn	|- J Fn ( S X. S )
18		ssid	|- { (/) } C_ { (/) }
19		snsspr1	|- { (/) } C_ { (/) , 1o }
20	3	setc1ohomfval	|- { <. (/) , (/) , 1o >. } = ( Hom ` E )
21		0lt1o	|- (/) e. 1o
22	21	a1i	|- ( T. -> (/) e. 1o )
23	4 15 20 22 22	homfval	|- ( T. -> ( (/) J (/) ) = ( (/) { <. (/) , (/) , 1o >. } (/) ) )
24	23	mptru	|- ( (/) J (/) ) = ( (/) { <. (/) , (/) , 1o >. } (/) )
25	10	ovsn2	|- ( (/) { <. (/) , (/) , 1o >. } (/) ) = 1o
26		df1o2	|- 1o = { (/) }
27	24 25 26	3eqtri	|- ( (/) J (/) ) = { (/) }
28		snex	|- { (/) } e. _V
29	1 28	catbas	|- { (/) } = ( Base ` C )
30		snex	|- { <. (/) , (/) , 2o >. } e. _V
31	1 30	cathomfval	|- { <. (/) , (/) , 2o >. } = ( Hom ` C )
32		0ex	|- (/) e. _V
33	32	snid	|- (/) e. { (/) }
34	33	a1i	|- ( T. -> (/) e. { (/) } )
35	6 29 31 34 34	homfval	|- ( T. -> ( (/) H (/) ) = ( (/) { <. (/) , (/) , 2o >. } (/) ) )
36	35	mptru	|- ( (/) H (/) ) = ( (/) { <. (/) , (/) , 2o >. } (/) )
37		2oex	|- 2o e. _V
38	37	ovsn2	|- ( (/) { <. (/) , (/) , 2o >. } (/) ) = 2o
39	36 38 11	3eqtri	|- ( (/) H (/) ) = { (/) , 1o }
40	19 27 39	3sstr4i	|- ( (/) J (/) ) C_ ( (/) H (/) )
41		oveq1	|- ( p = (/) -> ( p J q ) = ( (/) J q ) )
42		oveq1	|- ( p = (/) -> ( p H q ) = ( (/) H q ) )
43	41 42	sseq12d	|- ( p = (/) -> ( ( p J q ) C_ ( p H q ) <-> ( (/) J q ) C_ ( (/) H q ) ) )
44	43	ralbidv	|- ( p = (/) -> ( A. q e. { (/) } ( p J q ) C_ ( p H q ) <-> A. q e. { (/) } ( (/) J q ) C_ ( (/) H q ) ) )
45	32 44	ralsn	|- ( A. p e. { (/) } A. q e. { (/) } ( p J q ) C_ ( p H q ) <-> A. q e. { (/) } ( (/) J q ) C_ ( (/) H q ) )
46		oveq2	|- ( q = (/) -> ( (/) J q ) = ( (/) J (/) ) )
47		oveq2	|- ( q = (/) -> ( (/) H q ) = ( (/) H (/) ) )
48	46 47	sseq12d	|- ( q = (/) -> ( ( (/) J q ) C_ ( (/) H q ) <-> ( (/) J (/) ) C_ ( (/) H (/) ) ) )
49	32 48	ralsn	|- ( A. q e. { (/) } ( (/) J q ) C_ ( (/) H q ) <-> ( (/) J (/) ) C_ ( (/) H (/) ) )
50	45 49	bitri	|- ( A. p e. { (/) } A. q e. { (/) } ( p J q ) C_ ( p H q ) <-> ( (/) J (/) ) C_ ( (/) H (/) ) )
51	40 50	mpbir	|- A. p e. { (/) } A. q e. { (/) } ( p J q ) C_ ( p H q )
52	26 15	eqtr3i	|- { (/) } = ( Base ` E )
53	4 52	homffn	|- J Fn ( { (/) } X. { (/) } )
54	53	a1i	|- ( T. -> J Fn ( { (/) } X. { (/) } ) )
55	6 29	homffn	|- H Fn ( { (/) } X. { (/) } )
56	55	a1i	|- ( T. -> H Fn ( { (/) } X. { (/) } ) )
57	28	a1i	|- ( T. -> { (/) } e. _V )
58	54 56 57	isssc	|- ( T. -> ( J C_cat H <-> ( { (/) } C_ { (/) } /\ A. p e. { (/) } A. q e. { (/) } ( p J q ) C_ ( p H q ) ) ) )
59	58	mptru	|- ( J C_cat H <-> ( { (/) } C_ { (/) } /\ A. p e. { (/) } A. q e. { (/) } ( p J q ) C_ ( p H q ) ) )
60	18 51 59	mpbir2an	|- J C_cat H
61		elirr	|- -. { (/) } e. { (/) }
62	5 26	eqtri	|- S = { (/) }
63		biid	|- ( -. ( .1. ` x ) e. ( x J x ) <-> -. ( .1. ` x ) e. ( x J x ) )
64	62 63	rexeqbii	|- ( E. x e. S -. ( .1. ` x ) e. ( x J x ) <-> E. x e. { (/) } -. ( .1. ` x ) e. ( x J x ) )
65		rexnal	|- ( E. x e. S -. ( .1. ` x ) e. ( x J x ) <-> -. A. x e. S ( .1. ` x ) e. ( x J x ) )
66		fveq2	|- ( x = (/) -> ( .1. ` x ) = ( .1. ` (/) ) )
67	26	a1i	|- ( y = (/) -> 1o = { (/) } )
68	13	simpri	|- ( Id ` C ) = ( y e. { (/) } |-> 1o )
69	7 68	eqtri	|- .1. = ( y e. { (/) } |-> 1o )
70	67 69 28	fvmpt	|- ( (/) e. { (/) } -> ( .1. ` (/) ) = { (/) } )
71	33 70	ax-mp	|- ( .1. ` (/) ) = { (/) }
72	66 71	eqtrdi	|- ( x = (/) -> ( .1. ` x ) = { (/) } )
73		oveq12	|- ( ( x = (/) /\ x = (/) ) -> ( x J x ) = ( (/) J (/) ) )
74	73	anidms	|- ( x = (/) -> ( x J x ) = ( (/) J (/) ) )
75	74 27	eqtrdi	|- ( x = (/) -> ( x J x ) = { (/) } )
76	72 75	eleq12d	|- ( x = (/) -> ( ( .1. ` x ) e. ( x J x ) <-> { (/) } e. { (/) } ) )
77	76	notbid	|- ( x = (/) -> ( -. ( .1. ` x ) e. ( x J x ) <-> -. { (/) } e. { (/) } ) )
78	32 77	rexsn	|- ( E. x e. { (/) } -. ( .1. ` x ) e. ( x J x ) <-> -. { (/) } e. { (/) } )
79	64 65 78	3bitr3ri	|- ( -. { (/) } e. { (/) } <-> -. A. x e. S ( .1. ` x ) e. ( x J x ) )
80	61 79	mpbi	|- -. A. x e. S ( .1. ` x ) e. ( x J x )
81		setc1oterm	|- ( SetCat ` 1o ) e. TermCat
82	81	a1i	|- ( T. -> ( SetCat ` 1o ) e. TermCat )
83	82	termccd	|- ( T. -> ( SetCat ` 1o ) e. Cat )
84	83	mptru	|- ( SetCat ` 1o ) e. Cat
85	3 84	eqeltri	|- E e. Cat
86		snex	|- { <. <. (/) , (/) >. , (/) , .x. >. } e. _V
87	1 86	catcofval	|- { <. <. (/) , (/) >. , (/) , .x. >. } = ( comp ` C )
88	3	setc1ocofval	|- { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } = ( comp ` E )
89		velsn	|- ( a e. { (/) } <-> a = (/) )
90		velsn	|- ( b e. { (/) } <-> b = (/) )
91		velsn	|- ( c e. { (/) } <-> c = (/) )
92	89 90 91	3anbi123i	|- ( ( a e. { (/) } /\ b e. { (/) } /\ c e. { (/) } ) <-> ( a = (/) /\ b = (/) /\ c = (/) ) )
93	92	anbi1i	|- ( ( ( a e. { (/) } /\ b e. { (/) } /\ c e. { (/) } ) /\ ( m e. ( a J b ) /\ n e. ( b J c ) ) ) <-> ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m e. ( a J b ) /\ n e. ( b J c ) ) ) )
94		simp1	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> a = (/) )
95		simp2	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> b = (/) )
96	94 95	oveq12d	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( a J b ) = ( (/) J (/) ) )
97	96 27	eqtrdi	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( a J b ) = { (/) } )
98	97	eleq2d	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( m e. ( a J b ) <-> m e. { (/) } ) )
99		velsn	|- ( m e. { (/) } <-> m = (/) )
100	98 99	bitrdi	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( m e. ( a J b ) <-> m = (/) ) )
101		simp3	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> c = (/) )
102	95 101	oveq12d	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( b J c ) = ( (/) J (/) ) )
103	102 27	eqtrdi	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( b J c ) = { (/) } )
104	103	eleq2d	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( n e. ( b J c ) <-> n e. { (/) } ) )
105		velsn	|- ( n e. { (/) } <-> n = (/) )
106	104 105	bitrdi	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( n e. ( b J c ) <-> n = (/) ) )
107	100 106	anbi12d	|- ( ( a = (/) /\ b = (/) /\ c = (/) ) -> ( ( m e. ( a J b ) /\ n e. ( b J c ) ) <-> ( m = (/) /\ n = (/) ) ) )
108	107	pm5.32i	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m e. ( a J b ) /\ n e. ( b J c ) ) ) <-> ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) )
109	93 108	bitri	|- ( ( ( a e. { (/) } /\ b e. { (/) } /\ c e. { (/) } ) /\ ( m e. ( a J b ) /\ n e. ( b J c ) ) ) <-> ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) )
110	32	prid1	|- (/) e. { (/) , 1o }
111	110 11	eleqtrri	|- (/) e. 2o
112		ineq12	|- ( ( f = (/) /\ g = (/) ) -> ( f i^i g ) = ( (/) i^i (/) ) )
113		0in	|- ( (/) i^i (/) ) = (/)
114	112 113	eqtrdi	|- ( ( f = (/) /\ g = (/) ) -> ( f i^i g ) = (/) )
115	114 2 32	ovmpoa	|- ( ( (/) e. 2o /\ (/) e. 2o ) -> ( (/) .x. (/) ) = (/) )
116	111 111 115	mp2an	|- ( (/) .x. (/) ) = (/)
117	32	ovsn2	|- ( (/) { <. (/) , (/) , (/) >. } (/) ) = (/)
118	116 117	eqtr4i	|- ( (/) .x. (/) ) = ( (/) { <. (/) , (/) , (/) >. } (/) )
119		simpl1	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> a = (/) )
120		simpl2	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> b = (/) )
121	119 120	opeq12d	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> <. a , b >. = <. (/) , (/) >. )
122		simpl3	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> c = (/) )
123	121 122	oveq12d	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( <. a , b >. { <. <. (/) , (/) >. , (/) , .x. >. } c ) = ( <. (/) , (/) >. { <. <. (/) , (/) >. , (/) , .x. >. } (/) ) )
124	37 37	mpoex	|- ( f e. 2o , g e. 2o |-> ( f i^i g ) ) e. _V
125	2 124	eqeltri	|- .x. e. _V
126	125	ovsn2	|- ( <. (/) , (/) >. { <. <. (/) , (/) >. , (/) , .x. >. } (/) ) = .x.
127	123 126	eqtrdi	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( <. a , b >. { <. <. (/) , (/) >. , (/) , .x. >. } c ) = .x. )
128		simprr	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> n = (/) )
129		simprl	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> m = (/) )
130	127 128 129	oveq123d	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , .x. >. } c ) m ) = ( (/) .x. (/) ) )
131	121 122	oveq12d	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( <. a , b >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } c ) = ( <. (/) , (/) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } (/) ) )
132		snex	|- { <. (/) , (/) , (/) >. } e. _V
133	132	ovsn2	|- ( <. (/) , (/) >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } (/) ) = { <. (/) , (/) , (/) >. }
134	131 133	eqtrdi	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( <. a , b >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } c ) = { <. (/) , (/) , (/) >. } )
135	134 128 129	oveq123d	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } c ) m ) = ( (/) { <. (/) , (/) , (/) >. } (/) ) )
136	118 130 135	3eqtr4a	|- ( ( ( a = (/) /\ b = (/) /\ c = (/) ) /\ ( m = (/) /\ n = (/) ) ) -> ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , .x. >. } c ) m ) = ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } c ) m ) )
137	109 136	sylbi	|- ( ( ( a e. { (/) } /\ b e. { (/) } /\ c e. { (/) } ) /\ ( m e. ( a J b ) /\ n e. ( b J c ) ) ) -> ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , .x. >. } c ) m ) = ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } c ) m ) )
138	137	adantll	|- ( ( ( T. /\ ( a e. { (/) } /\ b e. { (/) } /\ c e. { (/) } ) ) /\ ( m e. ( a J b ) /\ n e. ( b J c ) ) ) -> ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , .x. >. } c ) m ) = ( n ( <. a , b >. { <. <. (/) , (/) >. , (/) , { <. (/) , (/) , (/) >. } >. } c ) m ) )
139	85	a1i	|- ( T. -> E e. Cat )
140	18	a1i	|- ( T. -> { (/) } C_ { (/) } )
141	8 29 52 4 87 88 138 139 140	resccat	|- ( T. -> ( D e. Cat <-> E e. Cat ) )
142	141	mptru	|- ( D e. Cat <-> E e. Cat )
143	85 142	mpbir	|- D e. Cat
144	60 80 143	3pm3.2i	|- ( J C_cat H /\ -. A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat )
145	14 17 144	3pm3.2i	|- ( C e. Cat /\ J Fn ( S X. S ) /\ ( J C_cat H /\ -. A. x e. S ( .1. ` x ) e. ( x J x ) /\ D e. Cat ) )