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

Metamath Proof Explorer

Theorem oppglt

Description: less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018)

Ref Expression
Hypotheses oppglt.1 ⊢ O = opp 𝑔 ⁡ R
oppglt.2 ⊢ < ˙ = < R
Assertion oppglt ⊢ R ∈ V → < ˙ = < O

Proof

Step Hyp Ref Expression
1 oppglt.1 ⊢ O = opp 𝑔 ⁡ R
2 oppglt.2 ⊢ < ˙ = < R
3 eqid ⊢ ≤ R = ≤ R
4 3 2 pltfval ⊢ R ∈ V → < ˙ = ≤ R ∖ I
5 1 fvexi ⊢ O ∈ V
6 1 3 oppgle ⊢ ≤ R = ≤ O
7 eqid ⊢ < O = < O
8 6 7 pltfval ⊢ O ∈ V → < O = ≤ R ∖ I
9 5 8 ax-mp ⊢ < O = ≤ R ∖ I
10 4 9 eqtr4di ⊢ R ∈ V → < ˙ = < O