Definition df-subc 17758

Description: (Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 19002, this is not actually a collection of categories (as in definition 4.1(a) of [Adamek] p. 48), but only sets which when given operations from the base category (using df-resc 17757) form a category. All the objects and all the morphisms of the subcategory belong to the supercategory. The identity of an object, the domain and the codomain of a morphism are the same in the subcategory and the supercategory. The composition of the subcategory is a restriction of the composition of the supercategory. (Contributed by FL, 17-Sep-2009.) (Revised by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
df-subc	⊢ Subcat = (𝑐 ∈ Cat ↦ {ℎ ∣ (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))})

Distinct variable group:   𝑓,𝑐,𝑔,ℎ,𝑠,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-subc

Step	Hyp	Ref	Expression
1		csubc 17755	. 2 class Subcat
2		vc	. . 3 setvar 𝑐
3		ccat 17607	. . 3 class Cat
4		vh	. . . . . . 7 setvar ℎ
5	4	cv 1540	. . . . . 6 class ℎ
6	2	cv 1540	. . . . . . 7 class 𝑐
7		chomf 17609	. . . . . . 7 class Homf
8	6, 7	cfv 6543	. . . . . 6 class (Homf ‘𝑐)
9		cssc 17753	. . . . . 6 class ⊆cat
10	5, 8, 9	wbr 5148	. . . . 5 wff ℎ ⊆cat (Homf ‘𝑐)
11		vx	. . . . . . . . . . 11 setvar 𝑥
12	11	cv 1540	. . . . . . . . . 10 class 𝑥
13		ccid 17608	. . . . . . . . . . 11 class Id
14	6, 13	cfv 6543	. . . . . . . . . 10 class (Id‘𝑐)
15	12, 14	cfv 6543	. . . . . . . . 9 class ((Id‘𝑐)‘𝑥)
16	12, 12, 5	co 7408	. . . . . . . . 9 class (𝑥ℎ𝑥)
17	15, 16	wcel 2106	. . . . . . . 8 wff ((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥)
18		vg	. . . . . . . . . . . . . . 15 setvar 𝑔
19	18	cv 1540	. . . . . . . . . . . . . 14 class 𝑔
20		vf	. . . . . . . . . . . . . . 15 setvar 𝑓
21	20	cv 1540	. . . . . . . . . . . . . 14 class 𝑓
22		vy	. . . . . . . . . . . . . . . . 17 setvar 𝑦
23	22	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑦
24	12, 23	cop 4634	. . . . . . . . . . . . . . 15 class ⟨𝑥, 𝑦⟩
25		vz	. . . . . . . . . . . . . . . 16 setvar 𝑧
26	25	cv 1540	. . . . . . . . . . . . . . 15 class 𝑧
27		cco 17208	. . . . . . . . . . . . . . . 16 class comp
28	6, 27	cfv 6543	. . . . . . . . . . . . . . 15 class (comp‘𝑐)
29	24, 26, 28	co 7408	. . . . . . . . . . . . . 14 class (⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)
30	19, 21, 29	co 7408	. . . . . . . . . . . . 13 class (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓)
31	12, 26, 5	co 7408	. . . . . . . . . . . . 13 class (𝑥ℎ𝑧)
32	30, 31	wcel 2106	. . . . . . . . . . . 12 wff (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)
33	23, 26, 5	co 7408	. . . . . . . . . . . 12 class (𝑦ℎ𝑧)
34	32, 18, 33	wral 3061	. . . . . . . . . . 11 wff ∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)
35	12, 23, 5	co 7408	. . . . . . . . . . 11 class (𝑥ℎ𝑦)
36	34, 20, 35	wral 3061	. . . . . . . . . 10 wff ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)
37		vs	. . . . . . . . . . 11 setvar 𝑠
38	37	cv 1540	. . . . . . . . . 10 class 𝑠
39	36, 25, 38	wral 3061	. . . . . . . . 9 wff ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)
40	39, 22, 38	wral 3061	. . . . . . . 8 wff ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)
41	17, 40	wa 396	. . . . . . 7 wff (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧))
42	41, 11, 38	wral 3061	. . . . . 6 wff ∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧))
43	5	cdm 5676	. . . . . . 7 class dom ℎ
44	43	cdm 5676	. . . . . 6 class dom dom ℎ
45	42, 37, 44	wsbc 3777	. . . . 5 wff [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧))
46	10, 45	wa 396	. . . 4 wff (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))
47	46, 4	cab 2709	. . 3 class {ℎ ∣ (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))}
48	2, 3, 47	cmpt 5231	. 2 class (𝑐 ∈ Cat ↦ {ℎ ∣ (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))})
49	1, 48	wceq 1541	1 wff Subcat = (𝑐 ∈ Cat ↦ {ℎ ∣ (ℎ ⊆cat (Homf ‘𝑐) ∧ [dom dom ℎ / 𝑠]∀𝑥 ∈ 𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥ℎ𝑥) ∧ ∀𝑦 ∈ 𝑠 ∀𝑧 ∈ 𝑠 ∀𝑓 ∈ (𝑥ℎ𝑦)∀𝑔 ∈ (𝑦ℎ𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥ℎ𝑧)))})

This definition is referenced by:  subcrcl  17762  issubc  17784