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 eqid ( +g𝑅 ) = ( +g𝑅 )
4 3 1 oppgval 𝑂 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g𝑅 ) ⟩ )
5 tsetid TopSet = Slot ( TopSet ‘ ndx )
6 tsetndxnplusgndx ( TopSet ‘ ndx ) ≠ ( +g ‘ ndx )
7 4 5 6 setsplusg ( TopSet ‘ 𝑅 ) = ( TopSet ‘ 𝑂 )
8 2 7 eqtri 𝐽 = ( TopSet ‘ 𝑂 )