Metamath Proof Explorer


Theorem oppgtset

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

Ref Expression
Hypotheses oppgbas.1 𝑂 = ( oppg𝑅 )
oppgtset.2 𝐽 = ( TopSet ‘ 𝑅 )
Assertion oppgtset 𝐽 = ( TopSet ‘ 𝑂 )

Proof

Step Hyp Ref Expression
1 oppgbas.1 𝑂 = ( oppg𝑅 )
2 oppgtset.2 𝐽 = ( TopSet ‘ 𝑅 )
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 ‘ 𝑅 ) = ( TopSet ‘ 𝑂 )
9 2 8 eqtri 𝐽 = ( TopSet ‘ 𝑂 )