Definition df-odu 17351

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

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 17410. (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 17350	. 2 class ODual
2		vw	. . 3 setvar 𝑤
3		cvv 3341	. . 3 class V
4	2	cv 1631	. . . 4 class 𝑤
5		cnx 16077	. . . . . 6 class ndx
6		cple 16171	. . . . . 6 class le
7	5, 6	cfv 6050	. . . . 5 class (le‘ndx)
8	4, 6	cfv 6050	. . . . . 6 class (le‘𝑤)
9	8	ccnv 5266	. . . . 5 class ◡(le‘𝑤)
10	7, 9	cop 4328	. . . 4 class ⟨(le‘ndx), ◡(le‘𝑤)⟩
11		csts 16078	. . . 4 class sSet
12	4, 10, 11	co 6815	. . 3 class (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩)
13	2, 3, 12	cmpt 4882	. 2 class (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))
14	1, 13	wceq 1632	1 wff ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))

This definition is referenced by:  oduval  17352