MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-subc Structured version   Visualization version   GIF version

Definition df-subc 17317
Description: (Subcat‘𝐶) is the set of all the subcategory specifications of the category 𝐶. Like df-subg 18540, 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 17316) 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
StepHypRef Expression
1 csubc 17314 . 2 class Subcat
2 vc . . 3 setvar 𝑐
3 ccat 17167 . . 3 class Cat
4 vh . . . . . . 7 setvar
54cv 1542 . . . . . 6 class
62cv 1542 . . . . . . 7 class 𝑐
7 chomf 17169 . . . . . . 7 class Homf
86, 7cfv 6380 . . . . . 6 class (Homf𝑐)
9 cssc 17312 . . . . . 6 class cat
105, 8, 9wbr 5053 . . . . 5 wff cat (Homf𝑐)
11 vx . . . . . . . . . . 11 setvar 𝑥
1211cv 1542 . . . . . . . . . 10 class 𝑥
13 ccid 17168 . . . . . . . . . . 11 class Id
146, 13cfv 6380 . . . . . . . . . 10 class (Id‘𝑐)
1512, 14cfv 6380 . . . . . . . . 9 class ((Id‘𝑐)‘𝑥)
1612, 12, 5co 7213 . . . . . . . . 9 class (𝑥𝑥)
1715, 16wcel 2110 . . . . . . . 8 wff ((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥)
18 vg . . . . . . . . . . . . . . 15 setvar 𝑔
1918cv 1542 . . . . . . . . . . . . . 14 class 𝑔
20 vf . . . . . . . . . . . . . . 15 setvar 𝑓
2120cv 1542 . . . . . . . . . . . . . 14 class 𝑓
22 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
2322cv 1542 . . . . . . . . . . . . . . . 16 class 𝑦
2412, 23cop 4547 . . . . . . . . . . . . . . 15 class 𝑥, 𝑦
25 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
2625cv 1542 . . . . . . . . . . . . . . 15 class 𝑧
27 cco 16814 . . . . . . . . . . . . . . . 16 class comp
286, 27cfv 6380 . . . . . . . . . . . . . . 15 class (comp‘𝑐)
2924, 26, 28co 7213 . . . . . . . . . . . . . 14 class (⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)
3019, 21, 29co 7213 . . . . . . . . . . . . 13 class (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓)
3112, 26, 5co 7213 . . . . . . . . . . . . 13 class (𝑥𝑧)
3230, 31wcel 2110 . . . . . . . . . . . 12 wff (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)
3323, 26, 5co 7213 . . . . . . . . . . . 12 class (𝑦𝑧)
3432, 18, 33wral 3061 . . . . . . . . . . 11 wff 𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)
3512, 23, 5co 7213 . . . . . . . . . . 11 class (𝑥𝑦)
3634, 20, 35wral 3061 . . . . . . . . . 10 wff 𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)
37 vs . . . . . . . . . . 11 setvar 𝑠
3837cv 1542 . . . . . . . . . 10 class 𝑠
3936, 25, 38wral 3061 . . . . . . . . 9 wff 𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)
4039, 22, 38wral 3061 . . . . . . . 8 wff 𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)
4117, 40wa 399 . . . . . . 7 wff (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧))
4241, 11, 38wral 3061 . . . . . 6 wff 𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧))
435cdm 5551 . . . . . . 7 class dom
4443cdm 5551 . . . . . 6 class dom dom
4542, 37, 44wsbc 3694 . . . . 5 wff [dom dom / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧))
4610, 45wa 399 . . . 4 wff (cat (Homf𝑐) ∧ [dom dom / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)))
4746, 4cab 2714 . . 3 class { ∣ (cat (Homf𝑐) ∧ [dom dom / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)))}
482, 3, 47cmpt 5135 . 2 class (𝑐 ∈ Cat ↦ { ∣ (cat (Homf𝑐) ∧ [dom dom / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)))})
491, 48wceq 1543 1 wff Subcat = (𝑐 ∈ Cat ↦ { ∣ (cat (Homf𝑐) ∧ [dom dom / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑦)∀𝑔 ∈ (𝑦𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑧)))})
Colors of variables: wff setvar class
This definition is referenced by:  subcrcl  17321  issubc  17341
  Copyright terms: Public domain W3C validator