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

Definition df-odu 14326
Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 14330, oduleval 14328, and oduleg 14329 for its principal properties.

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 14384. (Contributed by Stefan O'Rear, 29-Jan-2015.)

Assertion
Ref Expression
df-odu  |- ODual  =  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w )
>. ) )

Detailed syntax breakdown of Definition df-odu
StepHypRef Expression
1 codu 14325 . 2  class ODual
2 vw . . 3  set  w
3 cvv 2864 . . 3  class  _V
42cv 1641 . . . 4  class  w
5 cnx 13236 . . . . . 6  class  ndx
6 cple 13306 . . . . . 6  class  le
75, 6cfv 5334 . . . . 5  class  ( le
`  ndx )
84, 6cfv 5334 . . . . . 6  class  ( le
`  w )
98ccnv 4767 . . . . 5  class  `' ( le `  w )
107, 9cop 3719 . . . 4  class  <. ( le `  ndx ) ,  `' ( le `  w ) >.
11 csts 13237 . . . 4  class sSet
124, 10, 11co 5942 . . 3  class  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
)
132, 3, 12cmpt 4156 . 2  class  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
) )
141, 13wceq 1642 1  wff ODual  =  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w )
>. ) )
Colors of variables: wff set class
This definition is referenced by:  oduval  14327
  Copyright terms: Public domain W3C validator