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

Definition df-mon 16994
 Description: Function returning the monomorphisms of the category 𝑐. JFM CAT1 def. 10. (Contributed by FL, 5-Dec-2007.) (Revised by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-mon Mono = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
Distinct variable group:   𝑏,𝑐,𝑓,𝑔,,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-mon
StepHypRef Expression
1 cmon 16992 . 2 class Mono
2 vc . . 3 setvar 𝑐
3 ccat 16929 . . 3 class Cat
4 vb . . . 4 setvar 𝑏
52cv 1532 . . . . 5 class 𝑐
6 cbs 16477 . . . . 5 class Base
75, 6cfv 6349 . . . 4 class (Base‘𝑐)
8 vh . . . . 5 setvar
9 chom 16570 . . . . . 6 class Hom
105, 9cfv 6349 . . . . 5 class (Hom ‘𝑐)
11 vx . . . . . 6 setvar 𝑥
12 vy . . . . . 6 setvar 𝑦
134cv 1532 . . . . . 6 class 𝑏
14 vg . . . . . . . . . . 11 setvar 𝑔
15 vz . . . . . . . . . . . . 13 setvar 𝑧
1615cv 1532 . . . . . . . . . . . 12 class 𝑧
1711cv 1532 . . . . . . . . . . . 12 class 𝑥
188cv 1532 . . . . . . . . . . . 12 class
1916, 17, 18co 7150 . . . . . . . . . . 11 class (𝑧𝑥)
20 vf . . . . . . . . . . . . 13 setvar 𝑓
2120cv 1532 . . . . . . . . . . . 12 class 𝑓
2214cv 1532 . . . . . . . . . . . 12 class 𝑔
2316, 17cop 4566 . . . . . . . . . . . . 13 class 𝑧, 𝑥
2412cv 1532 . . . . . . . . . . . . 13 class 𝑦
25 cco 16571 . . . . . . . . . . . . . 14 class comp
265, 25cfv 6349 . . . . . . . . . . . . 13 class (comp‘𝑐)
2723, 24, 26co 7150 . . . . . . . . . . . 12 class (⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)
2821, 22, 27co 7150 . . . . . . . . . . 11 class (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔)
2914, 19, 28cmpt 5138 . . . . . . . . . 10 class (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3029ccnv 5548 . . . . . . . . 9 class (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3130wfun 6343 . . . . . . . 8 wff Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3231, 15, 13wral 3138 . . . . . . 7 wff 𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3317, 24, 18co 7150 . . . . . . 7 class (𝑥𝑦)
3432, 20, 33crab 3142 . . . . . 6 class {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}
3511, 12, 13, 13, 34cmpo 7152 . . . . 5 class (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
368, 10, 35csb 3882 . . . 4 class (Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
374, 7, 36csb 3882 . . 3 class (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
382, 3, 37cmpt 5138 . 2 class (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
391, 38wceq 1533 1 wff Mono = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
 Colors of variables: wff setvar class This definition is referenced by:  monfval  16996
 Copyright terms: Public domain W3C validator