Definition df-odu 18300

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

EDITORIAL: likely usable to simplify many lattice proofs, as it allows for duality arguments to be formalized; for instance latmass 18508. (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 18299	. 2 class ODual
2		vw	. . 3 setvar 𝑤
3		cvv 3453	. . 3 class V
4	2	cv 1558	. . . 4 class 𝑤
5		cnx 17210	. . . . . 6 class ndx
6		cple 17274	. . . . . 6 class le
7	5, 6	cfv 6515	. . . . 5 class (le‘ndx)
8	4, 6	cfv 6515	. . . . . 6 class (le‘𝑤)
9	8	ccnv 5644	. . . . 5 class ◡(le‘𝑤)
10	7, 9	cop 4587	. . . 4 class ⟨(le‘ndx), ◡(le‘𝑤)⟩
11		csts 17180	. . . 4 class sSet
12	4, 10, 11	co 7390	. . 3 class (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩)
13	2, 3, 12	cmpt 5180	. 2 class (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))
14	1, 13	wceq 1559	1 wff ODual = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(le‘ndx), ◡(le‘𝑤)⟩))

This definition is referenced by:  oduval  18301