Metamath Proof Explorer

Definition df-odu

Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas , oduleval , and oduleg for its principal properties.

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 codu
` |-  ODual`
1 vw
` |-  w`
2 cvv
` |-  _V`
3 1 cv
` |-  w`
4 csts
` |-  sSet`
5 cple
` |-  le`
6 cnx
` |-  ndx`
7 6 5 cfv
` |-  ( le ` ndx )`
8 3 5 cfv
` |-  ( le ` w )`
9 8 ccnv
` |-  `' ( le ` w )`
10 7 9 cop
` |-  <. ( le ` ndx ) , `' ( le ` w ) >.`
11 3 10 4 co
` |-  ( w sSet <. ( le ` ndx ) , `' ( le ` w ) >. )`
12 1 2 11 cmpt
` |-  ( w e. _V |-> ( w sSet <. ( le ` ndx ) , `' ( le ` w ) >. ) )`
13 0 12 wceq
` |-  ODual = ( w e. _V |-> ( w sSet <. ( le ` ndx ) , `' ( le ` w ) >. ) )`