Theorem oppgle

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

	Ref	Expression
Hypotheses	oppglt.1	|- O = ( oppG ` R )
	oppgle.2	|- .<_ = ( le ` R )
Assertion	oppgle	|- .<_ = ( le ` O )

Proof

Step	Hyp	Ref	Expression
1		oppglt.1	|- O = ( oppG ` R )
2		oppgle.2	|- .<_ = ( le ` R )
3		df-ple	|- le = Slot ; 1 0
4		10nn	|- ; 1 0 e. NN
5		2re	|- 2 e. RR
6		2lt10	|- 2 < ; 1 0
7	5 6	gtneii	|- ; 1 0 =/= 2
8	1 3 4 7	oppglem	|- ( le ` R ) = ( le ` O )
9	2 8	eqtri	|- .<_ = ( le ` O )