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 = ( ODual ` O )
	oduval.l	|- .<_ = ( le ` O )
	oduleg.g	|- G = ( le ` D )
Assertion	oduleg	|- ( ( A e. V /\ B e. W ) -> ( A G B <-> B .<_ A ) )

Proof

Step	Hyp	Ref	Expression
1		oduval.d	|- D = ( ODual ` O )
2		oduval.l	|- .<_ = ( le ` O )
3		oduleg.g	|- G = ( le ` D )
4	1 2	oduleval	|- `' .<_ = ( le ` D )
5	3 4	eqtr4i	|- G = `' .<_
6	5	breqi	|- ( A G B <-> A `' .<_ B )
7		brcnvg	|- ( ( A e. V /\ B e. W ) -> ( A `' .<_ B <-> B .<_ A ) )
8	6 7	bitrid	|- ( ( A e. V /\ B e. W ) -> ( A G B <-> B .<_ A ) )