Metamath Proof Explorer


Theorem oppgtset

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

Ref Expression
Hypotheses oppgbas.1 O = opp 𝑔 R
oppgtset.2 J = TopSet R
Assertion oppgtset J = TopSet O

Proof

Step Hyp Ref Expression
1 oppgbas.1 O = opp 𝑔 R
2 oppgtset.2 J = TopSet R
3 df-tset TopSet = Slot 9
4 9nn 9
5 2re 2
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