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