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

Definition df-odu 17069
Description: Define the dual of an ordered structure, which replaces the order component of the structure with its reverse. See odubas 17073, oduleval 17071, and oduleg 17072 for its principal properties.

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

Assertion
Ref Expression
df-odu ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), (le‘𝑤)⟩))

Detailed syntax breakdown of Definition df-odu
StepHypRef Expression
1 codu 17068 . 2 class ODual
2 vw . . 3 setvar 𝑤
3 cvv 3190 . . 3 class V
42cv 1479 . . . 4 class 𝑤
5 cnx 15797 . . . . . 6 class ndx
6 cple 15888 . . . . . 6 class le
75, 6cfv 5857 . . . . 5 class (le‘ndx)
84, 6cfv 5857 . . . . . 6 class (le‘𝑤)
98ccnv 5083 . . . . 5 class (le‘𝑤)
107, 9cop 4161 . . . 4 class ⟨(le‘ndx), (le‘𝑤)⟩
11 csts 15798 . . . 4 class sSet
124, 10, 11co 6615 . . 3 class (𝑤 sSet ⟨(le‘ndx), (le‘𝑤)⟩)
132, 3, 12cmpt 4683 . 2 class (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), (le‘𝑤)⟩))
141, 13wceq 1480 1 wff ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), (le‘𝑤)⟩))
Colors of variables: wff setvar class
This definition is referenced by:  oduval  17070
  Copyright terms: Public domain W3C validator