Metamath Proof Explorer

Definition df-mon

Description: Function returning the monomorphisms of the category c . JFM CAT_1 def. 10. (Contributed by FL, 5-Dec-2007) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-mon ⊢Mono=c∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌x∈b,y∈b⟼f∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmon classMono
1 vc setvarc
2 ccat classCat
3 cbs classBase
4 1 cv setvarc
5 4 3 cfv classBasec
6 vb setvarb
7 chom classHom
8 4 7 cfv classHom⁡c
9 vh setvarh
10 vx setvarx
11 6 cv setvarb
12 vy setvary
13 vf setvarf
14 10 cv setvarx
15 9 cv setvarh
16 12 cv setvary
17 14 16 15 co classxhy
18 vz setvarz
19 vg setvarg
20 18 cv setvarz
21 20 14 15 co classzhx
22 13 cv setvarf
23 20 14 cop classzx
24 cco classcomp
25 4 24 cfv classcomp⁡c
26 23 16 25 co classzxcomp⁡cy
27 19 cv setvarg
28 22 27 26 co classfzxcomp⁡cyg
29 19 21 28 cmpt classg∈zhx⟼fzxcomp⁡cyg
30 29 ccnv classg∈zhx⟼fzxcomp⁡cyg-1
31 30 wfun wffFun⁡g∈zhx⟼fzxcomp⁡cyg-1
32 31 18 11 wral wff∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1
33 32 13 17 crab classf∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1
34 10 12 11 11 33 cmpo classx∈b,y∈b⟼f∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1
35 9 8 34 csb class⦋Hom⁡c/h⦌x∈b,y∈b⟼f∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1
36 6 5 35 csb class⦋Basec/b⦌⦋Hom⁡c/h⦌x∈b,y∈b⟼f∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1
37 1 2 36 cmpt classc∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌x∈b,y∈b⟼f∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1
38 0 37 wceq wffMono=c∈Cat⟼⦋Basec/b⦌⦋Hom⁡c/h⦌x∈b,y∈b⟼f∈xhy|∀z∈bFun⁡g∈zhx⟼fzxcomp⁡cyg-1