Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-orhom Unicode version

Definition df-orhom 25209
 Description: Increasing functions also called "order homomorphisms", "isotone, monotone or order preserving mappings". To have the class of decreasing functions use . Experimental. Bourbaki E.III.7 (Contributed by FL, 17-Nov-2014.)
Assertion
Ref Expression
df-orhom
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-orhom
StepHypRef Expression
1 corhom 25207 . 2
2 vr . . 3
3 vs . . 3
4 cvv 2788 . . 3
5 va . . . . . . . . 9
65cv 1622 . . . . . . . 8
7 vb . . . . . . . . 9
87cv 1622 . . . . . . . 8
92cv 1622 . . . . . . . . 9
10 cple 13215 . . . . . . . . 9
119, 10cfv 5255 . . . . . . . 8
126, 8, 11wbr 4023 . . . . . . 7
13 vf . . . . . . . . . 10
1413cv 1622 . . . . . . . . 9
156, 14cfv 5255 . . . . . . . 8
168, 14cfv 5255 . . . . . . . 8
173cv 1622 . . . . . . . . 9
1817, 10cfv 5255 . . . . . . . 8
1915, 16, 18wbr 4023 . . . . . . 7
2012, 19wi 4 . . . . . 6
21 cbs 13148 . . . . . . 7
229, 21cfv 5255 . . . . . 6
2320, 7, 22wral 2543 . . . . 5
2423, 5, 22wral 2543 . . . 4
2517, 21cfv 5255 . . . . 5
26 cmap 6772 . . . . 5
2725, 22, 26co 5858 . . . 4
2824, 13, 27crab 2547 . . 3
292, 3, 4, 4, 28cmpt2 5860 . 2
301, 29wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  isorhom  25211
 Copyright terms: Public domain W3C validator