Users' Mathboxes 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  ( r  OrHom  `' s ). Experimental. Bourbaki E.III.7 (Contributed by FL, 17-Nov-2014.)
Assertion
Ref Expression
df-orhom  |-  OrHom  =  ( r  e.  _V , 
s  e.  _V  |->  { f  e.  ( (
Base `  s )  ^m  ( Base `  r
) )  |  A. a  e.  ( Base `  r ) A. b  e.  ( Base `  r
) ( a ( le `  r ) b  ->  ( f `  a ) ( le
`  s ) ( f `  b ) ) } )
Distinct variable group:    s, r, f, a, b

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