Metamath Proof Explorer

Definition 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 ∈ Cat ⟼ h | h ⊆ cat Hom 𝑓 ⁡ c ∧ [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ 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 ⊆ cat
6 chomf class Hom 𝑓
7 1 cv setvar c
8 7 6 cfv class Hom 𝑓 ⁡ c
9 4 8 5 wbr wff h ⊆ 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 ∈ 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 ∈ x h z
38 37 26 28 wral wff ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
39 38 23 25 wral wff ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
40 39 22 14 wral wff ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
41 40 21 14 wral wff ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
42 20 41 wa wff Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
43 42 13 14 wral wff ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
44 43 12 11 wsbc wff [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
45 9 44 wa wff h ⊆ cat Hom 𝑓 ⁡ c ∧ [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
46 45 3 cab class h | h ⊆ cat Hom 𝑓 ⁡ c ∧ [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
47 1 2 46 cmpt class c ∈ Cat ⟼ h | h ⊆ cat Hom 𝑓 ⁡ c ∧ [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
48 0 47 wceq wff Subcat = c ∈ Cat ⟼ h | h ⊆ cat Hom 𝑓 ⁡ c ∧ [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z