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 = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑤 ) ⟩ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | codu | ⊢ ODual | |
| 1 | vw | ⊢ 𝑤 | |
| 2 | cvv | ⊢ V | |
| 3 | 1 | cv | ⊢ 𝑤 |
| 4 | csts | ⊢ sSet | |
| 5 | cple | ⊢ le | |
| 6 | cnx | ⊢ ndx | |
| 7 | 6 5 | cfv | ⊢ ( le ‘ ndx ) |
| 8 | 3 5 | cfv | ⊢ ( le ‘ 𝑤 ) |
| 9 | 8 | ccnv | ⊢ ◡ ( le ‘ 𝑤 ) |
| 10 | 7 9 | cop | ⊢ ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑤 ) ⟩ |
| 11 | 3 10 4 | co | ⊢ ( 𝑤 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑤 ) ⟩ ) |
| 12 | 1 2 11 | cmpt | ⊢ ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑤 ) ⟩ ) ) |
| 13 | 0 12 | wceq | ⊢ ODual = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑤 ) ⟩ ) ) |