Theorem oppgleOLD

Description: Obsolete version of oppgle as of 27-Oct-2024. less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	oppglt.1	⊢ 𝑂 = ( oppg ‘ 𝑅 )
	oppgle.2	⊢ ≤ = ( le ‘ 𝑅 )
Assertion	oppgleOLD	⊢ ≤ = ( 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	oppglemOLD	⊢ ( le ‘ 𝑅 ) = ( le ‘ 𝑂 )
9	2 8	eqtri	⊢ ≤ = ( le ‘ 𝑂 )