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}, \{\emptyset\}⟩, ⟨Hom (ndx), \{⟨\emptyset, \emptyset, 2_{𝑜}⟩\}⟩, ⟨comp (ndx), \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \underset{˙}{\cdot}⟩\}⟩\}$
	setc1onsubc.x	$⊢ \underset{˙}{\cdot} = (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g)$
	setc1onsubc.e	$⊢ E = SetCat (1_{𝑜})$
	setc1onsubc.j	$⊢ J = {Hom}_{𝑓} (E)$
	setc1onsubc.s	$⊢ S = 1_{𝑜}$
	setc1onsubc.h	$⊢ H = {Hom}_{𝑓} (C)$
	setc1onsubc.i	$⊢ \underset{˙}{1} = Id (C)$
	setc1onsubc.d	$⊢ D = C ↾_{cat} J$
Assertion	setc1onsubc	$⊢ (C \in Cat \land J Fn (S \times S) \land (J \subseteq_{cat} H \land \neg \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat))$

Proof

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

Metamath Proof Explorer

Theorem setc1onsubc

Proof