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		df-tset	|- TopSet = Slot 9
4		9nn	|- 9 e. NN
5		2re	|- 2 e. RR
6		2lt9	|- 2 < 9
7	5 6	gtneii	|- 9 =/= 2
8	1 3 4 7	oppglem	|- ( TopSet ` R ) = ( TopSet ` O )
9	2 8	eqtri	|- J = ( TopSet ` O )