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

Definition df-odu 14587
Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 14591, oduleval 14589, and oduleg 14590 for its principal properties.

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 14645. (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 14586 . 2  class ODual
2 vw . . 3  set  w
3 cvv 2962 . . 3  class  _V
42cv 1652 . . . 4  class  w
5 cnx 13497 . . . . . 6  class  ndx
6 cple 13567 . . . . . 6  class  le
75, 6cfv 5483 . . . . 5  class  ( le
`  ndx )
84, 6cfv 5483 . . . . . 6  class  ( le
`  w )
98ccnv 4906 . . . . 5  class  `' ( le `  w )
107, 9cop 3841 . . . 4  class  <. ( le `  ndx ) ,  `' ( le `  w ) >.
11 csts 13498 . . . 4  class sSet
124, 10, 11co 6110 . . 3  class  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
)
132, 3, 12cmpt 4291 . 2  class  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
) )
141, 13wceq 1653 1  wff ODual  =  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w )
>. ) )
Colors of variables: wff set class
This definition is referenced by:  oduval  14588
  Copyright terms: Public domain W3C validator