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

Definition df-mon 16371
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 16369 . 2 class Mono
2 vc . . 3 setvar 𝑐
3 ccat 16306 . . 3 class Cat
4 vb . . . 4 setvar 𝑏
52cv 1480 . . . . 5 class 𝑐
6 cbs 15838 . . . . 5 class Base
75, 6cfv 5876 . . . 4 class (Base‘𝑐)
8 vh . . . . 5 setvar
9 chom 15933 . . . . . 6 class Hom
105, 9cfv 5876 . . . . 5 class (Hom ‘𝑐)
11 vx . . . . . 6 setvar 𝑥
12 vy . . . . . 6 setvar 𝑦
134cv 1480 . . . . . 6 class 𝑏
14 vg . . . . . . . . . . 11 setvar 𝑔
15 vz . . . . . . . . . . . . 13 setvar 𝑧
1615cv 1480 . . . . . . . . . . . 12 class 𝑧
1711cv 1480 . . . . . . . . . . . 12 class 𝑥
188cv 1480 . . . . . . . . . . . 12 class
1916, 17, 18co 6635 . . . . . . . . . . 11 class (𝑧𝑥)
20 vf . . . . . . . . . . . . 13 setvar 𝑓
2120cv 1480 . . . . . . . . . . . 12 class 𝑓
2214cv 1480 . . . . . . . . . . . 12 class 𝑔
2316, 17cop 4174 . . . . . . . . . . . . 13 class 𝑧, 𝑥
2412cv 1480 . . . . . . . . . . . . 13 class 𝑦
25 cco 15934 . . . . . . . . . . . . . 14 class comp
265, 25cfv 5876 . . . . . . . . . . . . 13 class (comp‘𝑐)
2723, 24, 26co 6635 . . . . . . . . . . . 12 class (⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)
2821, 22, 27co 6635 . . . . . . . . . . 11 class (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔)
2914, 19, 28cmpt 4720 . . . . . . . . . 10 class (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3029ccnv 5103 . . . . . . . . 9 class (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3130wfun 5870 . . . . . . . 8 wff Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3231, 15, 13wral 2909 . . . . . . 7 wff 𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
3317, 24, 18co 6635 . . . . . . 7 class (𝑥𝑦)
3432, 20, 33crab 2913 . . . . . 6 class {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}
3511, 12, 13, 13, 34cmpt2 6637 . . . . 5 class (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
368, 10, 35csb 3526 . . . 4 class (Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
374, 7, 36csb 3526 . . 3 class (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
382, 3, 37cmpt 4720 . 2 class (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
391, 38wceq 1481 1 wff Mono = (𝑐 ∈ Cat ↦ (Base‘𝑐) / 𝑏(Hom ‘𝑐) / (𝑥𝑏, 𝑦𝑏 ↦ {𝑓 ∈ (𝑥𝑦) ∣ ∀𝑧𝑏 Fun (𝑔 ∈ (𝑧𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
Colors of variables: wff setvar class
This definition is referenced by:  monfval  16373
  Copyright terms: Public domain W3C validator