Theorem oppgtset

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

	Ref	Expression
Hypotheses	oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
	oppgtset.2	$$⊢J=\mathrm{TopSet}\left(R\right)$$
Assertion	oppgtset	$$⊢J=\mathrm{TopSet}\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$$⊢O={opp}_{𝑔}\left(R\right)$$
2		oppgtset.2	$$⊢J=\mathrm{TopSet}\left(R\right)$$
3		df-tset	$$⊢\mathrm{TopSet}=\mathrm{Slot}9$$
4		9nn	$$⊢9\in \mathbb{N}$$
5		2re	$$⊢2\in ℝ$$
6		2lt9	$$⊢2<9$$
7	5 6	gtneii	$$⊢9\ne 2$$
8	1 3 4 7	oppglem	$$⊢\mathrm{TopSet}\left(R\right)=\mathrm{TopSet}\left(O\right)$$
9	2 8	eqtri	$$⊢J=\mathrm{TopSet}\left(O\right)$$