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	⊢ 𝐷 = ( ODual ‘ 𝑂 )
	oduval.l	⊢ ≤ = ( le ‘ 𝑂 )
	oduleg.g	⊢ 𝐺 = ( le ‘ 𝐷 )
Assertion	oduleg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 𝐺 𝐵 ↔ 𝐵 ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		oduval.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
2		oduval.l	⊢ ≤ = ( le ‘ 𝑂 )
3		oduleg.g	⊢ 𝐺 = ( le ‘ 𝐷 )
4	1 2	oduleval	⊢ ◡ ≤ = ( le ‘ 𝐷 )
5	3 4	eqtr4i	⊢ 𝐺 = ◡ ≤
6	5	breqi	⊢ ( 𝐴 𝐺 𝐵 ↔ 𝐴 ◡ ≤ 𝐵 )
7		brcnvg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ◡ ≤ 𝐵 ↔ 𝐵 ≤ 𝐴 ) )
8	6 7	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 𝐺 𝐵 ↔ 𝐵 ≤ 𝐴 ) )