Metamath Proof Explorer


Theorem oppgle

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

Ref Expression
Hypotheses oppglt.1 𝑂 = ( oppg𝑅 )
oppgle.2 = ( le ‘ 𝑅 )
Assertion oppgle = ( le ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppglt.1 𝑂 = ( oppg𝑅 )
2 oppgle.2 = ( le ‘ 𝑅 )
3 df-ple le = Slot 1 0
4 10nn 1 0 ∈ ℕ
5 2re 2 ∈ ℝ
6 2lt10 2 < 1 0
7 5 6 gtneii 1 0 ≠ 2
8 1 3 4 7 oppglem ( le ‘ 𝑅 ) = ( le ‘ 𝑂 )
9 2 8 eqtri = ( le ‘ 𝑂 )