This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 𝐺 𝐵 ↔ 𝐵 ≤ 𝐴 ) )