discsubc

Description: A discrete category, whose only morphisms are the identity morphisms, is a subcategory. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Hypotheses	discsubc.j	$⊢ J = (x \in S, y \in S ⟼ if (x = y, \{I (x)\}, \emptyset))$
	discsubc.b	$⊢ B = {Base}_{C}$
	discsubc.i	$⊢ I = Id (C)$
	discsubc.s	$⊢ φ \to S \subseteq B$
	discsubc.c	$⊢ φ \to C \in Cat$
Assertion	discsubc	$⊢ φ \to J \in Subcat (C)$

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	$⊢ J = (x \in S, y \in S ⟼ if (x = y, \{I (x)\}, \emptyset))$
2		discsubc.b	$⊢ B = {Base}_{C}$
3		discsubc.i	$⊢ I = Id (C)$
4		discsubc.s	$⊢ φ \to S \subseteq B$
5		discsubc.c	$⊢ φ \to C \in Cat$
6		eqeq12	$⊢ (x = a \land y = b) \to (x = y \leftrightarrow a = b)$
7		simpl	$⊢ (x = a \land y = b) \to x = a$
8	7	fveq2d	$⊢ (x = a \land y = b) \to I (x) = I (a)$
9	8	sneqd	$⊢ (x = a \land y = b) \to \{I (x)\} = \{I (a)\}$
10	6 9	ifbieq1d	$⊢ (x = a \land y = b) \to if (x = y, \{I (x)\}, \emptyset) = if (a = b, \{I (a)\}, \emptyset)$
11		snex	$⊢ \{I (a)\} \in V$
12		0ex	$⊢ \emptyset \in V$
13	11 12	ifex	$⊢ if (a = b, \{I (a)\}, \emptyset) \in V$
14	10 1 13	ovmpoa	$⊢ (a \in S \land b \in S) \to a J b = if (a = b, \{I (a)\}, \emptyset)$
15	14	adantl	$⊢ (φ \land (a \in S \land b \in S)) \to a J b = if (a = b, \{I (a)\}, \emptyset)$
16		sseq1	$⊢ \{I (a)\} = if (a = b, \{I (a)\}, \emptyset) \to (\{I (a)\} \subseteq a {Hom}_{𝑓} (C) b \leftrightarrow if (a = b, \{I (a)\}, \emptyset) \subseteq a {Hom}_{𝑓} (C) b)$
17		sseq1	$⊢ \emptyset = if (a = b, \{I (a)\}, \emptyset) \to (\emptyset \subseteq a {Hom}_{𝑓} (C) b \leftrightarrow if (a = b, \{I (a)\}, \emptyset) \subseteq a {Hom}_{𝑓} (C) b)$
18		eqid	$⊢ Hom (C) = Hom (C)$
19	5	ad2antrr	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to C \in Cat$
20	4	ad2antrr	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to S \subseteq B$
21		simplrl	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to a \in S$
22	20 21	sseldd	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to a \in B$
23	2 18 3 19 22	catidcl	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to I (a) \in (a Hom (C) a)$
24		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
25	24 2 18 22 22	homfval	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to a {Hom}_{𝑓} (C) a = a Hom (C) a$
26		simpr	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to a = b$
27	26	oveq2d	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to a {Hom}_{𝑓} (C) a = a {Hom}_{𝑓} (C) b$
28	25 27	eqtr3d	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to a Hom (C) a = a {Hom}_{𝑓} (C) b$
29	23 28	eleqtrd	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to I (a) \in (a {Hom}_{𝑓} (C) b)$
30	29	snssd	$⊢ ((φ \land (a \in S \land b \in S)) \land a = b) \to \{I (a)\} \subseteq a {Hom}_{𝑓} (C) b$
31		0ss	$⊢ \emptyset \subseteq a {Hom}_{𝑓} (C) b$
32	31	a1i	$⊢ ((φ \land (a \in S \land b \in S)) \land \neg a = b) \to \emptyset \subseteq a {Hom}_{𝑓} (C) b$
33	16 17 30 32	ifbothda	$⊢ (φ \land (a \in S \land b \in S)) \to if (a = b, \{I (a)\}, \emptyset) \subseteq a {Hom}_{𝑓} (C) b$
34	15 33	eqsstrd	$⊢ (φ \land (a \in S \land b \in S)) \to a J b \subseteq a {Hom}_{𝑓} (C) b$
35	34	ralrimivva	$⊢ φ \to \forall a \in S \forall b \in S a J b \subseteq a {Hom}_{𝑓} (C) b$
36	1	discsubclem	$⊢ J Fn (S \times S)$
37	36	a1i	$⊢ φ \to J Fn (S \times S)$
38	24 2	homffn	$⊢ {Hom}_{𝑓} (C) Fn (B \times B)$
39	38	a1i	$⊢ φ \to {Hom}_{𝑓} (C) Fn (B \times B)$
40	2	fvexi	$⊢ B \in V$
41	40	a1i	$⊢ φ \to B \in V$
42	37 39 41	isssc	$⊢ φ \to (J \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow (S \subseteq B \land \forall a \in S \forall b \in S a J b \subseteq a {Hom}_{𝑓} (C) b))$
43	4 35 42	mpbir2and	$⊢ φ \to J \subseteq_{cat} {Hom}_{𝑓} (C)$
44		fvex	$⊢ I (a) \in V$
45	44	snid	$⊢ I (a) \in \{I (a)\}$
46		simpr	$⊢ (φ \land a \in S) \to a \in S$
47		equtr2	$⊢ (x = a \land y = a) \to x = y$
48	47	iftrued	$⊢ (x = a \land y = a) \to if (x = y, \{I (x)\}, \emptyset) = \{I (x)\}$
49		simpl	$⊢ (x = a \land y = a) \to x = a$
50	49	fveq2d	$⊢ (x = a \land y = a) \to I (x) = I (a)$
51	50	sneqd	$⊢ (x = a \land y = a) \to \{I (x)\} = \{I (a)\}$
52	48 51	eqtrd	$⊢ (x = a \land y = a) \to if (x = y, \{I (x)\}, \emptyset) = \{I (a)\}$
53	52 1 11	ovmpoa	$⊢ (a \in S \land a \in S) \to a J a = \{I (a)\}$
54	46 46 53	syl2anc	$⊢ (φ \land a \in S) \to a J a = \{I (a)\}$
55	45 54	eleqtrrid	$⊢ (φ \land a \in S) \to I (a) \in (a J a)$
56	45	a1i	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to I (a) \in \{I (a)\}$
57		simprl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to f \in (a J b)$
58	46	ad2antrr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a \in S$
59		simplrl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to b \in S$
60	58 59 14	syl2anc	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a J b = if (a = b, \{I (a)\}, \emptyset)$
61	57 60	eleqtrd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to f \in if (a = b, \{I (a)\}, \emptyset)$
62	61	ne0d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to if (a = b, \{I (a)\}, \emptyset) \neq \emptyset$
63		iffalse	$⊢ \neg a = b \to if (a = b, \{I (a)\}, \emptyset) = \emptyset$
64	63	necon1ai	$⊢ if (a = b, \{I (a)\}, \emptyset) \neq \emptyset \to a = b$
65	62 64	syl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a = b$
66	65	opeq2d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to ⟨a, a⟩ = ⟨a, b⟩$
67		simprr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g \in (b J c)$
68		eqeq12	$⊢ (x = b \land y = c) \to (x = y \leftrightarrow b = c)$
69		simpl	$⊢ (x = b \land y = c) \to x = b$
70	69	fveq2d	$⊢ (x = b \land y = c) \to I (x) = I (b)$
71	70	sneqd	$⊢ (x = b \land y = c) \to \{I (x)\} = \{I (b)\}$
72	68 71	ifbieq1d	$⊢ (x = b \land y = c) \to if (x = y, \{I (x)\}, \emptyset) = if (b = c, \{I (b)\}, \emptyset)$
73		snex	$⊢ \{I (b)\} \in V$
74	73 12	ifex	$⊢ if (b = c, \{I (b)\}, \emptyset) \in V$
75	72 1 74	ovmpoa	$⊢ (b \in S \land c \in S) \to b J c = if (b = c, \{I (b)\}, \emptyset)$
76	75	ad2antlr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to b J c = if (b = c, \{I (b)\}, \emptyset)$
77	67 76	eleqtrd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g \in if (b = c, \{I (b)\}, \emptyset)$
78	77	ne0d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to if (b = c, \{I (b)\}, \emptyset) \neq \emptyset$
79		iffalse	$⊢ \neg b = c \to if (b = c, \{I (b)\}, \emptyset) = \emptyset$
80	79	necon1ai	$⊢ if (b = c, \{I (b)\}, \emptyset) \neq \emptyset \to b = c$
81	78 80	syl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to b = c$
82	65 81	eqtrd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a = c$
83	66 82	oveq12d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to ⟨a, a⟩ comp (C) a = ⟨a, b⟩ comp (C) c$
84	83	eqcomd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to ⟨a, b⟩ comp (C) c = ⟨a, a⟩ comp (C) a$
85	81	iftrued	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to if (b = c, \{I (b)\}, \emptyset) = \{I (b)\}$
86	77 85	eleqtrd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g \in \{I (b)\}$
87	86	elsnd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g = I (b)$
88	65	fveq2d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to I (a) = I (b)$
89	87 88	eqtr4d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g = I (a)$
90	65	iftrued	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to if (a = b, \{I (a)\}, \emptyset) = \{I (a)\}$
91	61 90	eleqtrd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to f \in \{I (a)\}$
92	91	elsnd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to f = I (a)$
93	84 89 92	oveq123d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g (⟨a, b⟩ comp (C) c) f = I (a) (⟨a, a⟩ comp (C) a) I (a)$
94	5	ad3antrrr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to C \in Cat$
95	4	ad3antrrr	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to S \subseteq B$
96	95 58	sseldd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a \in B$
97		eqid	$⊢ comp (C) = comp (C)$
98	2 18 3 94 96	catidcl	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to I (a) \in (a Hom (C) a)$
99	2 18 3 94 96 97 96 98	catlid	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to I (a) (⟨a, a⟩ comp (C) a) I (a) = I (a)$
100	93 99	eqtrd	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g (⟨a, b⟩ comp (C) c) f = I (a)$
101	82	oveq2d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a J a = a J c$
102	58 58 53	syl2anc	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a J a = \{I (a)\}$
103	101 102	eqtr3d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to a J c = \{I (a)\}$
104	56 100 103	3eltr4d	$⊢ (((φ \land a \in S) \land (b \in S \land c \in S)) \land (f \in (a J b) \land g \in (b J c))) \to g (⟨a, b⟩ comp (C) c) f \in (a J c)$
105	104	ralrimivva	$⊢ ((φ \land a \in S) \land (b \in S \land c \in S)) \to \forall f \in (a J b) \forall g \in (b J c) g (⟨a, b⟩ comp (C) c) f \in (a J c)$
106	105	ralrimivva	$⊢ (φ \land a \in S) \to \forall b \in S \forall c \in S \forall f \in (a J b) \forall g \in (b J c) g (⟨a, b⟩ comp (C) c) f \in (a J c)$
107	55 106	jca	$⊢ (φ \land a \in S) \to (I (a) \in (a J a) \land \forall b \in S \forall c \in S \forall f \in (a J b) \forall g \in (b J c) g (⟨a, b⟩ comp (C) c) f \in (a J c))$
108	107	ralrimiva	$⊢ φ \to \forall a \in S (I (a) \in (a J a) \land \forall b \in S \forall c \in S \forall f \in (a J b) \forall g \in (b J c) g (⟨a, b⟩ comp (C) c) f \in (a J c))$
109	24 3 97 5 37	issubc2	$⊢ φ \to (J \in Subcat (C) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \forall a \in S (I (a) \in (a J a) \land \forall b \in S \forall c \in S \forall f \in (a J b) \forall g \in (b J c) g (⟨a, b⟩ comp (C) c) f \in (a J c))))$
110	43 108 109	mpbir2and	$⊢ φ \to J \in Subcat (C)$

Metamath Proof Explorer

Theorem discsubc

Proof