Definition df-odu 18320

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

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18528. (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

Step	Hyp	Ref	Expression
1		codu 18319	. 2 class ODual
2		vw	. . 3 setvar 𝑤
3		cvv 3455	. . 3 class V
4	2	cv 1560	. . . 4 class 𝑤
5		cnx 17230	. . . . . 6 class ndx
6		cple 17294	. . . . . 6 class le
7	5, 6	cfv 6522	. . . . 5 class (le‘ndx)
8	4, 6	cfv 6522	. . . . . 6 class (le‘𝑤)
9	8	ccnv 5647	. . . . 5 class ◡(le‘𝑤)
10	7, 9	cop 4589	. . . 4 class ⟨(le‘ndx), ◡(le‘𝑤)⟩
11		csts 17200	. . . 4 class sSet
12	4, 10, 11	co 7397	. . 3 class (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩)
13	2, 3, 12	cmpt 5182	. 2 class (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))
14	1, 13	wceq 1561	1 wff ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))

This definition is referenced by:  oduval  18321