Theorem oppgbas

Description: Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypotheses	oppgbas.1	|- O = ( oppG ` R )
	oppgbas.2	|- B = ( Base ` R )
Assertion	oppgbas	|- B = ( Base ` O )

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	|- O = ( oppG ` R )
2		oppgbas.2	|- B = ( Base ` R )
3		eqid	|- ( +g ` R ) = ( +g ` R )
4	3 1	oppgval	|- O = ( R sSet <. ( +g ` ndx ) , tpos ( +g ` R ) >. )
5		baseid	|- Base = Slot ( Base ` ndx )
6		basendxnplusgndx	|- ( Base ` ndx ) =/= ( +g ` ndx )
7	4 5 6	setsplusg	|- ( Base ` R ) = ( Base ` O )
8	2 7	eqtri	|- B = ( Base ` O )