Theorem oppgtset

Description: Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015)

	Ref	Expression
Hypotheses	oppgbas.1	|- O = ( oppG ` R )
	oppgtset.2	|- J = ( TopSet ` R )
Assertion	oppgtset	|- J = ( TopSet ` O )

Proof

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