Definition df-odu

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	$$⊢\mathrm{ODual}=\left(w\in \mathrm{V}⟼w\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_w}^{-1}⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		codu	$$class\mathrm{ODual}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarw$$
4		csts	$$class\mathrm{sSet}$$
5		cple	$$class\mathrm{le}$$
6		cnx	$$class\mathrm{ndx}$$
7	6 5	cfv	$$class{\le }_{\mathrm{ndx}}$$
8	3 5	cfv	$$class{\le }_w$$
9	8	ccnv	$$class{{\le }_w}^{-1}$$
10	7 9	cop	$$class⟨{\le }_{\mathrm{ndx}},{{\le }_w}^{-1}⟩$$
11	3 10 4	co	$$class\left(w\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_w}^{-1}⟩\right)$$
12	1 2 11	cmpt	$$class\left(w\in \mathrm{V}⟼w\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_w}^{-1}⟩\right)$$
13	0 12	wceq	$$wff\mathrm{ODual}=\left(w\in \mathrm{V}⟼w\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_w}^{-1}⟩\right)$$