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

Definition df-odu 14233
Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 14237, oduleval 14235, and oduleg 14236 for its principal properties.

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 14291. (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 14232 . 2  class ODual
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . 4  class  w
5 cnx 13145 . . . . . 6  class  ndx
6 cple 13215 . . . . . 6  class  le
75, 6cfv 5255 . . . . 5  class  ( le
`  ndx )
84, 6cfv 5255 . . . . . 6  class  ( le
`  w )
98ccnv 4688 . . . . 5  class  `' ( le `  w )
107, 9cop 3643 . . . 4  class  <. ( le `  ndx ) ,  `' ( le `  w ) >.
11 csts 13146 . . . 4  class sSet
124, 10, 11co 5858 . . 3  class  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
)
132, 3, 12cmpt 4077 . 2  class  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
) )
141, 13wceq 1623 1  wff ODual  =  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w )
>. ) )
Colors of variables: wff set class
This definition is referenced by:  oduval  14234
  Copyright terms: Public domain W3C validator