Theorem oduleg

Description: Truth of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	oduval.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
	oduval.l	$$⊢\underset{\dot{}}{\le }={\le }_O$$
	oduleg.g	$$⊢G={\le }_D$$
Assertion	oduleg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(AGB\leftrightarrow B\underset{\dot{}}{\le }A\right)$$

Proof

Step	Hyp	Ref	Expression
1		oduval.d	$$⊢D=\mathrm{ODual}\left(O\right)$$
2		oduval.l	$$⊢\underset{\dot{}}{\le }={\le }_O$$
3		oduleg.g	$$⊢G={\le }_D$$
4	1 2	oduleval	$$⊢{\underset{\dot{}}{\le }}^{-1}={\le }_D$$
5	3 4	eqtr4i	$$⊢G={\underset{\dot{}}{\le }}^{-1}$$
6	5	breqi	$$⊢AGB\leftrightarrow A{\underset{\dot{}}{\le }}^{-1}B$$
7		brcnvg	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A{\underset{\dot{}}{\le }}^{-1}B\leftrightarrow B\underset{\dot{}}{\le }A\right)$$
8	6 7	bitrid	$$⊢\left(A\in V\wedge B\in W\right)\to \left(AGB\leftrightarrow B\underset{\dot{}}{\le }A\right)$$