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 ) >. ) ) |
| 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 ) >. ) ) |