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 17702
Description: (Subcatβ€˜πΆ) is the set of all the subcategory specifications of the category 𝐢. Like df-subg 18932, 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 17701) 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 17699 . 2 class Subcat
2 vc . . 3 setvar 𝑐
3 ccat 17551 . . 3 class Cat
4 vh . . . . . . 7 setvar β„Ž
54cv 1541 . . . . . 6 class β„Ž
62cv 1541 . . . . . . 7 class 𝑐
7 chomf 17553 . . . . . . 7 class Homf
86, 7cfv 6501 . . . . . 6 class (Homf β€˜π‘)
9 cssc 17697 . . . . . 6 class βŠ†cat
105, 8, 9wbr 5110 . . . . 5 wff β„Ž βŠ†cat (Homf β€˜π‘)
11 vx . . . . . . . . . . 11 setvar π‘₯
1211cv 1541 . . . . . . . . . 10 class π‘₯
13 ccid 17552 . . . . . . . . . . 11 class Id
146, 13cfv 6501 . . . . . . . . . 10 class (Idβ€˜π‘)
1512, 14cfv 6501 . . . . . . . . 9 class ((Idβ€˜π‘)β€˜π‘₯)
1612, 12, 5co 7362 . . . . . . . . 9 class (π‘₯β„Žπ‘₯)
1715, 16wcel 2107 . . . . . . . 8 wff ((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯)
18 vg . . . . . . . . . . . . . . 15 setvar 𝑔
1918cv 1541 . . . . . . . . . . . . . 14 class 𝑔
20 vf . . . . . . . . . . . . . . 15 setvar 𝑓
2120cv 1541 . . . . . . . . . . . . . 14 class 𝑓
22 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
2322cv 1541 . . . . . . . . . . . . . . . 16 class 𝑦
2412, 23cop 4597 . . . . . . . . . . . . . . 15 class ⟨π‘₯, π‘¦βŸ©
25 vz . . . . . . . . . . . . . . . 16 setvar 𝑧
2625cv 1541 . . . . . . . . . . . . . . 15 class 𝑧
27 cco 17152 . . . . . . . . . . . . . . . 16 class comp
286, 27cfv 6501 . . . . . . . . . . . . . . 15 class (compβ€˜π‘)
2924, 26, 28co 7362 . . . . . . . . . . . . . 14 class (⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)
3019, 21, 29co 7362 . . . . . . . . . . . . 13 class (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓)
3112, 26, 5co 7362 . . . . . . . . . . . . 13 class (π‘₯β„Žπ‘§)
3230, 31wcel 2107 . . . . . . . . . . . 12 wff (𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)
3323, 26, 5co 7362 . . . . . . . . . . . 12 class (π‘¦β„Žπ‘§)
3432, 18, 33wral 3065 . . . . . . . . . . 11 wff βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)
3512, 23, 5co 7362 . . . . . . . . . . 11 class (π‘₯β„Žπ‘¦)
3634, 20, 35wral 3065 . . . . . . . . . 10 wff βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)
37 vs . . . . . . . . . . 11 setvar 𝑠
3837cv 1541 . . . . . . . . . 10 class 𝑠
3936, 25, 38wral 3065 . . . . . . . . 9 wff βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)
4039, 22, 38wral 3065 . . . . . . . 8 wff βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)
4117, 40wa 397 . . . . . . 7 wff (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§))
4241, 11, 38wral 3065 . . . . . 6 wff βˆ€π‘₯ ∈ 𝑠 (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§))
435cdm 5638 . . . . . . 7 class dom β„Ž
4443cdm 5638 . . . . . 6 class dom dom β„Ž
4542, 37, 44wsbc 3744 . . . . 5 wff [dom dom β„Ž / 𝑠]βˆ€π‘₯ ∈ 𝑠 (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§))
4610, 45wa 397 . . . 4 wff (β„Ž βŠ†cat (Homf β€˜π‘) ∧ [dom dom β„Ž / 𝑠]βˆ€π‘₯ ∈ 𝑠 (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)))
4746, 4cab 2714 . . 3 class {β„Ž ∣ (β„Ž βŠ†cat (Homf β€˜π‘) ∧ [dom dom β„Ž / 𝑠]βˆ€π‘₯ ∈ 𝑠 (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)))}
482, 3, 47cmpt 5193 . 2 class (𝑐 ∈ Cat ↦ {β„Ž ∣ (β„Ž βŠ†cat (Homf β€˜π‘) ∧ [dom dom β„Ž / 𝑠]βˆ€π‘₯ ∈ 𝑠 (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)))})
491, 48wceq 1542 1 wff Subcat = (𝑐 ∈ Cat ↦ {β„Ž ∣ (β„Ž βŠ†cat (Homf β€˜π‘) ∧ [dom dom β„Ž / 𝑠]βˆ€π‘₯ ∈ 𝑠 (((Idβ€˜π‘)β€˜π‘₯) ∈ (π‘₯β„Žπ‘₯) ∧ βˆ€π‘¦ ∈ 𝑠 βˆ€π‘§ ∈ 𝑠 βˆ€π‘“ ∈ (π‘₯β„Žπ‘¦)βˆ€π‘” ∈ (π‘¦β„Žπ‘§)(𝑔(⟨π‘₯, π‘¦βŸ©(compβ€˜π‘)𝑧)𝑓) ∈ (π‘₯β„Žπ‘§)))})
Colors of variables: wff setvar class
This definition is referenced by:  subcrcl  17706  issubc  17728
  Copyright terms: Public domain W3C validator