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

Definition df-odu 14515
Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 14519, oduleval 14517, and oduleg 14518 for its principal properties.

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 14573. (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 14514 . 2  class ODual
2 vw . . 3  set  w
3 cvv 2920 . . 3  class  _V
42cv 1648 . . . 4  class  w
5 cnx 13425 . . . . . 6  class  ndx
6 cple 13495 . . . . . 6  class  le
75, 6cfv 5417 . . . . 5  class  ( le
`  ndx )
84, 6cfv 5417 . . . . . 6  class  ( le
`  w )
98ccnv 4840 . . . . 5  class  `' ( le `  w )
107, 9cop 3781 . . . 4  class  <. ( le `  ndx ) ,  `' ( le `  w ) >.
11 csts 13426 . . . 4  class sSet
124, 10, 11co 6044 . . 3  class  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
)
132, 3, 12cmpt 4230 . 2  class  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
) )
141, 13wceq 1649 1  wff ODual  =  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w )
>. ) )
Colors of variables: wff set class
This definition is referenced by:  oduval  14516
  Copyright terms: Public domain W3C validator