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

Definition df-mon 14989
 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 14987 . 2 Mono
2 vc . . 3
3 ccat 14922 . . 3
4 vb . . . 4
52cv 1378 . . . . 5
6 cbs 14493 . . . . 5
75, 6cfv 5588 . . . 4
8 vh . . . . 5
9 chom 14569 . . . . . 6
105, 9cfv 5588 . . . . 5
11 vx . . . . . 6
12 vy . . . . . 6
134cv 1378 . . . . . 6
14 vg . . . . . . . . . . 11
15 vz . . . . . . . . . . . . 13
1615cv 1378 . . . . . . . . . . . 12
1711cv 1378 . . . . . . . . . . . 12
188cv 1378 . . . . . . . . . . . 12
1916, 17, 18co 6285 . . . . . . . . . . 11
20 vf . . . . . . . . . . . . 13
2120cv 1378 . . . . . . . . . . . 12
2214cv 1378 . . . . . . . . . . . 12
2316, 17cop 4033 . . . . . . . . . . . . 13
2412cv 1378 . . . . . . . . . . . . 13
25 cco 14570 . . . . . . . . . . . . . 14 comp
265, 25cfv 5588 . . . . . . . . . . . . 13 comp
2723, 24, 26co 6285 . . . . . . . . . . . 12 comp
2821, 22, 27co 6285 . . . . . . . . . . 11 comp
2914, 19, 28cmpt 4505 . . . . . . . . . 10 comp
3029ccnv 4998 . . . . . . . . 9 comp
3130wfun 5582 . . . . . . . 8 comp
3231, 15, 13wral 2814 . . . . . . 7 comp
3317, 24, 18co 6285 . . . . . . 7
3432, 20, 33crab 2818 . . . . . 6 comp
3511, 12, 13, 13, 34cmpt2 6287 . . . . 5 comp
368, 10, 35csb 3435 . . . 4 comp
374, 7, 36csb 3435 . . 3 comp
382, 3, 37cmpt 4505 . 2 comp
391, 38wceq 1379 1 Mono comp
 Colors of variables: wff setvar class This definition is referenced by:  monfval  14991
 Copyright terms: Public domain W3C validator