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=TopSetR
Assertion oppgtset J=TopSetO

Proof

Step Hyp Ref Expression
1 oppgbas.1 O=opp𝑔R
2 oppgtset.2 J=TopSetR
3 eqid +R=+R
4 3 1 oppgval O=RsSet+ndxtpos+R
5 tsetid TopSet=SlotTopSetndx
6 tsetndxnplusgndx TopSetndx+ndx
7 4 5 6 setsplusg TopSetR=TopSetO
8 2 7 eqtri J=TopSetO