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		elirr	$⊢ \neg \{\emptyset\} \in \{\emptyset\}$
62	5 26	eqtri	$⊢ S = \{\emptyset\}$
63		biid	$⊢ \neg \underset{˙}{1} (x) \in (x J x) \leftrightarrow \neg \underset{˙}{1} (x) \in (x J x)$
64	62 63	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)$
65		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)$
66		fveq2	$⊢ x = \emptyset \to \underset{˙}{1} (x) = \underset{˙}{1} (\emptyset)$
67	26	a1i	$⊢ y = \emptyset \to 1_{𝑜} = \{\emptyset\}$
68	13	simpri	$⊢ Id (C) = (y \in \{\emptyset\} ⟼ 1_{𝑜})$
69	7 68	eqtri	$⊢ \underset{˙}{1} = (y \in \{\emptyset\} ⟼ 1_{𝑜})$
70	67 69 28	fvmpt	$⊢ \emptyset \in \{\emptyset\} \to \underset{˙}{1} (\emptyset) = \{\emptyset\}$
71	33 70	ax-mp	$⊢ \underset{˙}{1} (\emptyset) = \{\emptyset\}$
72	66 71	eqtrdi	$⊢ x = \emptyset \to \underset{˙}{1} (x) = \{\emptyset\}$
73		oveq12	$⊢ (x = \emptyset \land x = \emptyset) \to x J x = \emptyset J \emptyset$
74	73	anidms	$⊢ x = \emptyset \to x J x = \emptyset J \emptyset$
75	74 27	eqtrdi	$⊢ x = \emptyset \to x J x = \{\emptyset\}$
76	72 75	eleq12d	$⊢ x = \emptyset \to (\underset{˙}{1} (x) \in (x J x) \leftrightarrow \{\emptyset\} \in \{\emptyset\})$
77	76	notbid	$⊢ x = \emptyset \to (\neg \underset{˙}{1} (x) \in (x J x) \leftrightarrow \neg \{\emptyset\} \in \{\emptyset\})$
78	32 77	rexsn	$⊢ \exists x \in \{\emptyset\} \neg \underset{˙}{1} (x) \in (x J x) \leftrightarrow \neg \{\emptyset\} \in \{\emptyset\}$
79	64 65 78	3bitr3ri	$⊢ \neg \{\emptyset\} \in \{\emptyset\} \leftrightarrow \neg \forall x \in S \underset{˙}{1} (x) \in (x J x)$
80	61 79	mpbi	$⊢ \neg \forall x \in S \underset{˙}{1} (x) \in (x J x)$
81		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for \|- ( SetCat ` 1o ) e. TermCat with typecode \|-
82	81	a1i	Could not format ( T. -> ( SetCat ` 1o ) e. TermCat ) : No typesetting found for \|- ( T. -> ( SetCat ` 1o ) e. TermCat ) with typecode \|-
83	82	termccd	$⊢ ⊤ \to SetCat (1_{𝑜}) \in Cat$
84	83	mptru	$⊢ SetCat (1_{𝑜}) \in Cat$
85	3 84	eqeltri	$⊢ E \in Cat$
86		snex	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \underset{˙}{\cdot}⟩\} \in V$
87	1 86	catcofval	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \underset{˙}{\cdot}⟩\} = comp (C)$
88	3	setc1ocofval	$⊢ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} = comp (E)$
89		velsn	$⊢ a \in \{\emptyset\} \leftrightarrow a = \emptyset$
90		velsn	$⊢ b \in \{\emptyset\} \leftrightarrow b = \emptyset$
91		velsn	$⊢ c \in \{\emptyset\} \leftrightarrow c = \emptyset$
92	89 90 91	3anbi123i	$⊢ (a \in \{\emptyset\} \land b \in \{\emptyset\} \land c \in \{\emptyset\}) \leftrightarrow (a = \emptyset \land b = \emptyset \land c = \emptyset)$
93	92	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)))$
94		simp1	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to a = \emptyset$
95		simp2	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to b = \emptyset$
96	94 95	oveq12d	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to a J b = \emptyset J \emptyset$
97	96 27	eqtrdi	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to a J b = \{\emptyset\}$
98	97	eleq2d	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to (m \in (a J b) \leftrightarrow m \in \{\emptyset\})$
99		velsn	$⊢ m \in \{\emptyset\} \leftrightarrow m = \emptyset$
100	98 99	bitrdi	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to (m \in (a J b) \leftrightarrow m = \emptyset)$
101		simp3	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to c = \emptyset$
102	95 101	oveq12d	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to b J c = \emptyset J \emptyset$
103	102 27	eqtrdi	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to b J c = \{\emptyset\}$
104	103	eleq2d	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to (n \in (b J c) \leftrightarrow n \in \{\emptyset\})$
105		velsn	$⊢ n \in \{\emptyset\} \leftrightarrow n = \emptyset$
106	104 105	bitrdi	$⊢ (a = \emptyset \land b = \emptyset \land c = \emptyset) \to (n \in (b J c) \leftrightarrow n = \emptyset)$
107	100 106	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))$
108	107	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))$
109	93 108	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))$
110	32	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
111	110 11	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
112		ineq12	$⊢ (f = \emptyset \land g = \emptyset) \to f \cap g = \emptyset \cap \emptyset$
113		0in	$⊢ \emptyset \cap \emptyset = \emptyset$
114	112 113	eqtrdi	$⊢ (f = \emptyset \land g = \emptyset) \to f \cap g = \emptyset$
115	114 2 32	ovmpoa	$⊢ (\emptyset \in 2_{𝑜} \land \emptyset \in 2_{𝑜}) \to \emptyset \underset{˙}{\cdot} \emptyset = \emptyset$
116	111 111 115	mp2an	$⊢ \emptyset \underset{˙}{\cdot} \emptyset = \emptyset$
117	32	ovsn2	$⊢ \emptyset \{⟨\emptyset, \emptyset, \emptyset⟩\} \emptyset = \emptyset$
118	116 117	eqtr4i	$⊢ \emptyset \underset{˙}{\cdot} \emptyset = \emptyset \{⟨\emptyset, \emptyset, \emptyset⟩\} \emptyset$
119		simpl1	$⊢ ((a = \emptyset \land b = \emptyset \land c = \emptyset) \land (m = \emptyset \land n = \emptyset)) \to a = \emptyset$
120		simpl2	$⊢ ((a = \emptyset \land b = \emptyset \land c = \emptyset) \land (m = \emptyset \land n = \emptyset)) \to b = \emptyset$
121	119 120	opeq12d	$⊢ ((a = \emptyset \land b = \emptyset \land c = \emptyset) \land (m = \emptyset \land n = \emptyset)) \to ⟨a, b⟩ = ⟨\emptyset, \emptyset⟩$
122		simpl3	$⊢ ((a = \emptyset \land b = \emptyset \land c = \emptyset) \land (m = \emptyset \land n = \emptyset)) \to c = \emptyset$
123	121 122	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$
124	37 37	mpoex	$⊢ (f \in 2_{𝑜}, g \in 2_{𝑜} ⟼ f \cap g) \in V$
125	2 124	eqeltri	$⊢ \underset{˙}{\cdot} \in V$
126	125	ovsn2	$⊢ ⟨\emptyset, \emptyset⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \underset{˙}{\cdot}⟩\} \emptyset = \underset{˙}{\cdot}$
127	123 126	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}$
128		simprr	$⊢ ((a = \emptyset \land b = \emptyset \land c = \emptyset) \land (m = \emptyset \land n = \emptyset)) \to n = \emptyset$
129		simprl	$⊢ ((a = \emptyset \land b = \emptyset \land c = \emptyset) \land (m = \emptyset \land n = \emptyset)) \to m = \emptyset$
130	127 128 129	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$
131	121 122	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$
132		snex	$⊢ \{⟨\emptyset, \emptyset, \emptyset⟩\} \in V$
133	132	ovsn2	$⊢ ⟨\emptyset, \emptyset⟩ \{⟨⟨\emptyset, \emptyset⟩, \emptyset, \{⟨\emptyset, \emptyset, \emptyset⟩\}⟩\} \emptyset = \{⟨\emptyset, \emptyset, \emptyset⟩\}$
134	131 133	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⟩\}$
135	134 128 129	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$
136	118 130 135	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$
137	109 136	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$
138	137	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$
139	85	a1i	$⊢ ⊤ \to E \in Cat$
140	18	a1i	$⊢ ⊤ \to \{\emptyset\} \subseteq \{\emptyset\}$
141	8 29 52 4 87 88 138 139 140	resccat	$⊢ ⊤ \to (D \in Cat \leftrightarrow E \in Cat)$
142	141	mptru	$⊢ D \in Cat \leftrightarrow E \in Cat$
143	85 142	mpbir	$⊢ D \in Cat$
144	60 80 143	3pm3.2i	$⊢ (J \subseteq_{cat} H \land \neg \forall x \in S \underset{˙}{1} (x) \in (x J x) \land D \in Cat)$
145	14 17 144	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