Theorem oppglt

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

	Ref	Expression
Hypotheses	oppglt.1	|- O = ( oppG ` R )
	oppglt.2	|- .< = ( lt ` R )
Assertion	oppglt	|- ( R e. V -> .< = ( lt ` O ) )

Proof

Step	Hyp	Ref	Expression
1		oppglt.1	|- O = ( oppG ` R )
2		oppglt.2	|- .< = ( lt ` R )
3		eqid	|- ( le ` R ) = ( le ` R )
4	3 2	pltfval	|- ( R e. V -> .< = ( ( le ` R ) \ _I ) )
5	1	fvexi	|- O e. _V
6	1 3	oppgle	|- ( le ` R ) = ( le ` O )
7		eqid	|- ( lt ` O ) = ( lt ` O )
8	6 7	pltfval	|- ( O e. _V -> ( lt ` O ) = ( ( le ` R ) \ _I ) )
9	5 8	ax-mp	|- ( lt ` O ) = ( ( le ` R ) \ _I )
10	4 9	eqtr4di	|- ( R e. V -> .< = ( lt ` O ) )