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

Definition df-mon 13961
 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 comp
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-mon
StepHypRef Expression
1 cmon 13959 . 2 Mono
2 vc . . 3
3 ccat 13894 . . 3
4 vb . . . 4
52cv 1652 . . . . 5
6 cbs 13474 . . . . 5
75, 6cfv 5457 . . . 4
8 vh . . . . 5
9 chom 13545 . . . . . 6
105, 9cfv 5457 . . . . 5
11 vx . . . . . 6
12 vy . . . . . 6
134cv 1652 . . . . . 6
14 vg . . . . . . . . . . 11
15 vz . . . . . . . . . . . . 13
1615cv 1652 . . . . . . . . . . . 12
1711cv 1652 . . . . . . . . . . . 12
188cv 1652 . . . . . . . . . . . 12
1916, 17, 18co 6084 . . . . . . . . . . 11
20 vf . . . . . . . . . . . . 13
2120cv 1652 . . . . . . . . . . . 12
2214cv 1652 . . . . . . . . . . . 12
2316, 17cop 3819 . . . . . . . . . . . . 13
2412cv 1652 . . . . . . . . . . . . 13
25 cco 13546 . . . . . . . . . . . . . 14 comp
265, 25cfv 5457 . . . . . . . . . . . . 13 comp
2723, 24, 26co 6084 . . . . . . . . . . . 12 comp
2821, 22, 27co 6084 . . . . . . . . . . 11 comp
2914, 19, 28cmpt 4269 . . . . . . . . . 10 comp
3029ccnv 4880 . . . . . . . . 9 comp
3130wfun 5451 . . . . . . . 8 comp
3231, 15, 13wral 2707 . . . . . . 7 comp
3317, 24, 18co 6084 . . . . . . 7
3432, 20, 33crab 2711 . . . . . 6 comp
3511, 12, 13, 13, 34cmpt2 6086 . . . . 5 comp
368, 10, 35csb 3253 . . . 4 comp
374, 7, 36csb 3253 . . 3 comp
382, 3, 37cmpt 4269 . 2 comp
391, 38wceq 1653 1 Mono comp
 Colors of variables: wff set class This definition is referenced by:  monfval  13963
 Copyright terms: Public domain W3C validator