df-subc

Description: ( SubcatC ) is the set of all the subcategory specifications of the category C . Like df-subg , 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 ) 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)

		Ref	Expression
	Assertion	df-subc	$⊢ Subcat = (c \in Cat ⟼ \{h \| (h \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom h / s \underset{˙}{]} \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csubc	$class Subcat$
1		vc	$setvar c$
2		ccat	$class Cat$
3		vh	$setvar h$
4	3	cv	$setvar h$
5		cssc	$class \subseteq_{cat}$
6		chomf	$class {Hom}_{𝑓}$
7	1	cv	$setvar c$
8	7 6	cfv	$class {Hom}_{𝑓} (c)$
9	4 8 5	wbr	$wff h \subseteq_{cat} {Hom}_{𝑓} (c)$
10	4	cdm	$class dom h$
11	10	cdm	$class dom dom h$
12		vs	$setvar s$
13		vx	$setvar x$
14	12	cv	$setvar s$
15		ccid	$class Id$
16	7 15	cfv	$class Id (c)$
17	13	cv	$setvar x$
18	17 16	cfv	$class Id (c) (x)$
19	17 17 4	co	$class (x h x)$
20	18 19	wcel	$wff Id (c) (x) \in (x h x)$
21		vy	$setvar y$
22		vz	$setvar z$
23		vf	$setvar f$
24	21	cv	$setvar y$
25	17 24 4	co	$class (x h y)$
26		vg	$setvar g$
27	22	cv	$setvar z$
28	24 27 4	co	$class (y h z)$
29	26	cv	$setvar g$
30	17 24	cop	$class ⟨x, y⟩$
31		cco	$class comp$
32	7 31	cfv	$class comp (c)$
33	30 27 32	co	$class (⟨x, y⟩ comp (c) z)$
34	23	cv	$setvar f$
35	29 34 33	co	$class (g (⟨x, y⟩ comp (c) z) f)$
36	17 27 4	co	$class (x h z)$
37	35 36	wcel	$wff g (⟨x, y⟩ comp (c) z) f \in (x h z)$
38	37 26 28	wral	$wff \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)$
39	38 23 25	wral	$wff \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)$
40	39 22 14	wral	$wff \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)$
41	40 21 14	wral	$wff \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)$
42	20 41	wa	$wff (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z))$
43	42 13 14	wral	$wff \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z))$
44	43 12 11	wsbc	$wff \underset{˙}{[} dom dom h / s \underset{˙}{]} \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z))$
45	9 44	wa	$wff (h \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom h / s \underset{˙}{]} \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)))$
46	45 3	cab	$class \{h \| (h \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom h / s \underset{˙}{]} \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)))\}$
47	1 2 46	cmpt	$class (c \in Cat ⟼ \{h \| (h \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom h / s \underset{˙}{]} \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)))\})$
48	0 47	wceq	$wff Subcat = (c \in Cat ⟼ \{h \| (h \subseteq_{cat} {Hom}_{𝑓} (c) \land \underset{˙}{[} dom dom h / s \underset{˙}{]} \forall x \in s (Id (c) (x) \in (x h x) \land \forall y \in s \forall z \in s \forall f \in (x h y) \forall g \in (y h z) g (⟨x, y⟩ comp (c) z) f \in (x h z)))\})$

Metamath Proof Explorer

Definition df-subc

Detailed syntax breakdown