Definition df-mon 17867

Description: Function returning the monomorphisms of the category 𝑐. JFM CAT₁ 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

Step	Hyp	Ref	Expression
1		cmon 17865	. 2 class Mono
2		vc	. . 3 setvar 𝑐
3		ccat 17800	. . 3 class Cat
4		vb	. . . 4 setvar 𝑏
5	2	cv 1569	. . . . 5 class 𝑐
6		cbs 17349	. . . . 5 class Base
7	5, 6	cfv 6527	. . . 4 class (Base‘𝑐)
8		vh	. . . . 5 setvar ℎ
9		chom 17401	. . . . . 6 class Hom
10	5, 9	cfv 6527	. . . . 5 class (Hom ‘𝑐)
11		vx	. . . . . 6 setvar 𝑥
12		vy	. . . . . 6 setvar 𝑦
13	4	cv 1569	. . . . . 6 class 𝑏
14		vg	. . . . . . . . . . 11 setvar 𝑔
15		vz	. . . . . . . . . . . . 13 setvar 𝑧
16	15	cv 1569	. . . . . . . . . . . 12 class 𝑧
17	11	cv 1569	. . . . . . . . . . . 12 class 𝑥
18	8	cv 1569	. . . . . . . . . . . 12 class ℎ
19	16, 17, 18	co 7408	. . . . . . . . . . 11 class (𝑧ℎ𝑥)
20		vf	. . . . . . . . . . . . 13 setvar 𝑓
21	20	cv 1569	. . . . . . . . . . . 12 class 𝑓
22	14	cv 1569	. . . . . . . . . . . 12 class 𝑔
23	16, 17	cop 4589	. . . . . . . . . . . . 13 class ⟨𝑧, 𝑥⟩
24	12	cv 1569	. . . . . . . . . . . . 13 class 𝑦
25		cco 17402	. . . . . . . . . . . . . 14 class comp
26	5, 25	cfv 6527	. . . . . . . . . . . . 13 class (comp‘𝑐)
27	23, 24, 26	co 7408	. . . . . . . . . . . 12 class (⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)
28	21, 22, 27	co 7408	. . . . . . . . . . 11 class (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔)
29	14, 19, 28	cmpt 5185	. . . . . . . . . 10 class (𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
30	29	ccnv 5646	. . . . . . . . 9 class ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
31	30	wfun 6521	. . . . . . . 8 wff Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
32	31, 15, 13	wral 3076	. . . . . . 7 wff ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))
33	17, 24, 18	co 7408	. . . . . . 7 class (𝑥ℎ𝑦)
34	32, 20, 33	crab 3412	. . . . . 6 class {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}
35	11, 12, 13, 13, 34	cmpo 7410	. . . . 5 class (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
36	8, 10, 35	csb 3846	. . . 4 class ⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
37	4, 7, 36	csb 3846	. . 3 class ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))})
38	2, 3, 37	cmpt 5185	. 2 class (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))
39	1, 38	wceq 1570	1 wff Mono = (𝑐 ∈ Cat ↦ ⦋(Base‘𝑐) / 𝑏⦌⦋(Hom ‘𝑐) / ℎ⦌(𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ {𝑓 ∈ (𝑥ℎ𝑦) ∣ ∀𝑧 ∈ 𝑏 Fun ◡(𝑔 ∈ (𝑧ℎ𝑥) ↦ (𝑓(⟨𝑧, 𝑥⟩(comp‘𝑐)𝑦)𝑔))}))

This definition is used by:  monfval  17869