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

Definition df-odu 15628
Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 15632, oduleval 15630, and oduleg 15631 for its principal properties.

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 15687. (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 15627 . 2  class ODual
2 vw . . 3  setvar  w
3 cvv 3118 . . 3  class  _V
42cv 1378 . . . 4  class  w
5 cnx 14499 . . . . . 6  class  ndx
6 cple 14574 . . . . . 6  class  le
75, 6cfv 5593 . . . . 5  class  ( le
`  ndx )
84, 6cfv 5593 . . . . . 6  class  ( le
`  w )
98ccnv 5003 . . . . 5  class  `' ( le `  w )
107, 9cop 4038 . . . 4  class  <. ( le `  ndx ) ,  `' ( le `  w ) >.
11 csts 14500 . . . 4  class sSet
124, 10, 11co 6294 . . 3  class  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
)
132, 3, 12cmpt 4510 . 2  class  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w ) >.
) )
141, 13wceq 1379 1  wff ODual  =  ( w  e.  _V  |->  ( w sSet  <. ( le `  ndx ) ,  `' ( le `  w )
>. ) )
Colors of variables: wff setvar class
This definition is referenced by:  oduval  15629
  Copyright terms: Public domain W3C validator