ssccatid

Description: A category C restricted by J is a category if all of the following are satisfied: a) the base is a subset of base of C , b) all hom-sets are subsets of hom-sets of C , c) it has identity morphisms for all objects, d) the composition under C is closed in J . But J might not be a subcategory of C (see cnelsubc ). (Contributed by Zhi Wang, 6-Nov-2025)

	Ref	Expression
Hypotheses	ssccatid.h	$⊢ H = {Hom}_{𝑓} (C)$
	ssccatid.d	$⊢ D = C ↾_{cat} J$
	ssccatid.x	$⊢ \underset{˙}{\cdot} = comp (C)$
	ssccatid.j	$⊢ φ \to J \subseteq_{cat} H$
	ssccatid.f	$⊢ φ \to J Fn (S \times S)$
	ssccatid.c	$⊢ φ \to C \in Cat$
	ssccatid.i	$⊢ (φ \land y \in S) \to \underset{˙}{1} \in (y J y)$
	ssccatid.l	$⊢ (φ \land (a \in S \land b \in S \land m \in (a J b))) \to \underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = m$
	ssccatid.r	$⊢ (φ \land (a \in S \land b \in S \land m \in (a J b))) \to m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m$
	ssccatid.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z)$
Assertion	ssccatid	$⊢ φ \to (D \in Cat \land Id (D) = (y \in S ⟼ \underset{˙}{1}))$

Proof

Step	Hyp	Ref	Expression
1		ssccatid.h	$⊢ H = {Hom}_{𝑓} (C)$
2		ssccatid.d	$⊢ D = C ↾_{cat} J$
3		ssccatid.x	$⊢ \underset{˙}{\cdot} = comp (C)$
4		ssccatid.j	$⊢ φ \to J \subseteq_{cat} H$
5		ssccatid.f	$⊢ φ \to J Fn (S \times S)$
6		ssccatid.c	$⊢ φ \to C \in Cat$
7		ssccatid.i	$⊢ (φ \land y \in S) \to \underset{˙}{1} \in (y J y)$
8		ssccatid.l	$⊢ (φ \land (a \in S \land b \in S \land m \in (a J b))) \to \underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = m$
9		ssccatid.r	$⊢ (φ \land (a \in S \land b \in S \land m \in (a J b))) \to m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m$
10		ssccatid.1	$⊢ (φ \land (x \in S \land y \in S \land z \in S) \land (f \in (x J y) \land g \in (y J z))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z)$
11		eqid	$⊢ {Base}_{C} = {Base}_{C}$
12	1 11	homffn	$⊢ H Fn ({Base}_{C} \times {Base}_{C})$
13	12	a1i	$⊢ φ \to H Fn ({Base}_{C} \times {Base}_{C})$
14	5 13 4	ssc1	$⊢ φ \to S \subseteq {Base}_{C}$
15	2 11 6 5 14	rescbas	$⊢ φ \to S = {Base}_{D}$
16	2 11 6 5 14	reschom	$⊢ φ \to J = Hom (D)$
17	2 11 6 5 14 3	rescco	$⊢ φ \to \underset{˙}{\cdot} = comp (D)$
18	2	ovexi	$⊢ D \in V$
19	18	a1i	$⊢ φ \to D \in V$
20		biid	$⊢ ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w))) \leftrightarrow ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))$
21		oveq2	$⊢ m = f \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) m = \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f$
22		id	$⊢ m = f \to m = f$
23	21 22	eqeq12d	$⊢ m = f \to (\underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) m = m \leftrightarrow \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f)$
24		oveq1	$⊢ a = x \to a J b = x J b$
25		opeq1	$⊢ a = x \to ⟨a, b⟩ = ⟨x, b⟩$
26	25	oveq1d	$⊢ a = x \to ⟨a, b⟩ \underset{˙}{\cdot} b = ⟨x, b⟩ \underset{˙}{\cdot} b$
27	26	oveqd	$⊢ a = x \to \underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = \underset{˙}{1} (⟨x, b⟩ \underset{˙}{\cdot} b) m$
28	27	eqeq1d	$⊢ a = x \to (\underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = m \leftrightarrow \underset{˙}{1} (⟨x, b⟩ \underset{˙}{\cdot} b) m = m)$
29	24 28	raleqbidv	$⊢ a = x \to (\forall m \in (a J b) \underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = m \leftrightarrow \forall m \in (x J b) \underset{˙}{1} (⟨x, b⟩ \underset{˙}{\cdot} b) m = m)$
30		oveq2	$⊢ b = y \to x J b = x J y$
31		opeq2	$⊢ b = y \to ⟨x, b⟩ = ⟨x, y⟩$
32		id	$⊢ b = y \to b = y$
33	31 32	oveq12d	$⊢ b = y \to ⟨x, b⟩ \underset{˙}{\cdot} b = ⟨x, y⟩ \underset{˙}{\cdot} y$
34	33	oveqd	$⊢ b = y \to \underset{˙}{1} (⟨x, b⟩ \underset{˙}{\cdot} b) m = \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) m$
35	34	eqeq1d	$⊢ b = y \to (\underset{˙}{1} (⟨x, b⟩ \underset{˙}{\cdot} b) m = m \leftrightarrow \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) m = m)$
36	30 35	raleqbidv	$⊢ b = y \to (\forall m \in (x J b) \underset{˙}{1} (⟨x, b⟩ \underset{˙}{\cdot} b) m = m \leftrightarrow \forall m \in (x J y) \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) m = m)$
37	8	ralrimivvva	$⊢ φ \to \forall a \in S \forall b \in S \forall m \in (a J b) \underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = m$
38	37	adantr	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to \forall a \in S \forall b \in S \forall m \in (a J b) \underset{˙}{1} (⟨a, b⟩ \underset{˙}{\cdot} b) m = m$
39		simpr1l	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to x \in S$
40		simpr1r	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to y \in S$
41	29 36 38 39 40	rspc2dv	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to \forall m \in (x J y) \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) m = m$
42		simpr31	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to f \in (x J y)$
43	23 41 42	rspcdva	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to \underset{˙}{1} (⟨x, y⟩ \underset{˙}{\cdot} y) f = f$
44		oveq1	$⊢ m = g \to m (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1}$
45		id	$⊢ m = g \to m = g$
46	44 45	eqeq12d	$⊢ m = g \to (m (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = m \leftrightarrow g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g)$
47		oveq1	$⊢ a = y \to a J b = y J b$
48		id	$⊢ a = y \to a = y$
49	48 48	opeq12d	$⊢ a = y \to ⟨a, a⟩ = ⟨y, y⟩$
50	49	oveq1d	$⊢ a = y \to ⟨a, a⟩ \underset{˙}{\cdot} b = ⟨y, y⟩ \underset{˙}{\cdot} b$
51	50	oveqd	$⊢ a = y \to m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m (⟨y, y⟩ \underset{˙}{\cdot} b) \underset{˙}{1}$
52	51	eqeq1d	$⊢ a = y \to (m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m \leftrightarrow m (⟨y, y⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m)$
53	47 52	raleqbidv	$⊢ a = y \to (\forall m \in (a J b) m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m \leftrightarrow \forall m \in (y J b) m (⟨y, y⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m)$
54		oveq2	$⊢ b = z \to y J b = y J z$
55		oveq2	$⊢ b = z \to ⟨y, y⟩ \underset{˙}{\cdot} b = ⟨y, y⟩ \underset{˙}{\cdot} z$
56	55	oveqd	$⊢ b = z \to m (⟨y, y⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1}$
57	56	eqeq1d	$⊢ b = z \to (m (⟨y, y⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m \leftrightarrow m (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = m)$
58	54 57	raleqbidv	$⊢ b = z \to (\forall m \in (y J b) m (⟨y, y⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m \leftrightarrow \forall m \in (y J z) m (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = m)$
59	9	ralrimivvva	$⊢ φ \to \forall a \in S \forall b \in S \forall m \in (a J b) m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m$
60	59	adantr	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to \forall a \in S \forall b \in S \forall m \in (a J b) m (⟨a, a⟩ \underset{˙}{\cdot} b) \underset{˙}{1} = m$
61		simpr2l	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to z \in S$
62	53 58 60 40 61	rspc2dv	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to \forall m \in (y J z) m (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = m$
63		simpr32	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to g \in (y J z)$
64	46 62 63	rspcdva	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to g (⟨y, y⟩ \underset{˙}{\cdot} z) \underset{˙}{1} = g$
65		simpl	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to φ$
66	65 39 40 61 42 63 10	syl132anc	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to g (⟨x, y⟩ \underset{˙}{\cdot} z) f \in (x J z)$
67		eqid	$⊢ Hom (C) = Hom (C)$
68	6	adantr	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to C \in Cat$
69	14	adantr	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to S \subseteq {Base}_{C}$
70	69 39	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to x \in {Base}_{C}$
71	69 40	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to y \in {Base}_{C}$
72	69 61	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to z \in {Base}_{C}$
73	5	adantr	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to J Fn (S \times S)$
74	4	adantr	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to J \subseteq_{cat} H$
75	73 74 39 40	ssc2	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to x J y \subseteq x H y$
76	75 42	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to f \in (x H y)$
77	1 11 67 70 71	homfval	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to x H y = x Hom (C) y$
78	76 77	eleqtrd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to f \in (x Hom (C) y)$
79	73 74 40 61	ssc2	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to y J z \subseteq y H z$
80	79 63	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to g \in (y H z)$
81	1 11 67 71 72	homfval	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to y H z = y Hom (C) z$
82	80 81	eleqtrd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to g \in (y Hom (C) z)$
83		simpr2r	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to w \in S$
84	69 83	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to w \in {Base}_{C}$
85	73 74 61 83	ssc2	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to z J w \subseteq z H w$
86		simpr33	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to k \in (z J w)$
87	85 86	sseldd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to k \in (z H w)$
88	1 11 67 72 84	homfval	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to z H w = z Hom (C) w$
89	87 88	eleqtrd	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to k \in (z Hom (C) w)$
90	11 67 3 68 70 71 72 78 82 84 89	catass	$⊢ (φ \land ((x \in S \land y \in S) \land (z \in S \land w \in S) \land (f \in (x J y) \land g \in (y J z) \land k \in (z J w)))) \to (k (⟨y, z⟩ \underset{˙}{\cdot} w) g) (⟨x, y⟩ \underset{˙}{\cdot} w) f = k (⟨x, z⟩ \underset{˙}{\cdot} w) (g (⟨x, y⟩ \underset{˙}{\cdot} z) f)$
91	15 16 17 19 20 7 43 64 66 90	iscatd2	$⊢ φ \to (D \in Cat \land Id (D) = (y \in S ⟼ \underset{˙}{1}))$

Metamath Proof Explorer

Theorem ssccatid

Proof