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	$⊢ \underset{˙}{\leq} = \leq_{O}$
	oduleg.g	$⊢ G = \leq_{D}$
Assertion	oduleg	$⊢ (A \in V \land B \in W) \to (A G B \leftrightarrow B \underset{˙}{\leq} A)$

Step	Hyp	Ref	Expression
1		oduval.d	$⊢ D = ODual (O)$
2		oduval.l	$⊢ \underset{˙}{\leq} = \leq_{O}$
3		oduleg.g	$⊢ G = \leq_{D}$
4	1 2	oduleval	$⊢ {\underset{˙}{\leq}}^{-1} = \leq_{D}$
5	3 4	eqtr4i	$⊢ G = {\underset{˙}{\leq}}^{-1}$
6	5	breqi	$⊢ A G B \leftrightarrow A {\underset{˙}{\leq}}^{-1} B$
7		brcnvg	$⊢ (A \in V \land B \in W) \to (A {\underset{˙}{\leq}}^{-1} B \leftrightarrow B \underset{˙}{\leq} A)$
8	6 7	bitrid	$⊢ (A \in V \land B \in W) \to (A G B \leftrightarrow B \underset{˙}{\leq} A)$

Metamath Proof Explorer