Metamath Proof Explorer


Theorem oppgtopn

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

Ref Expression
Hypotheses oppgbas.1 O=opp𝑔R
oppgtopn.2 J=TopOpenR
Assertion oppgtopn J=TopOpenO

Proof

Step Hyp Ref Expression
1 oppgbas.1 O=opp𝑔R
2 oppgtopn.2 J=TopOpenR
3 eqid BaseR=BaseR
4 eqid TopSetR=TopSetR
5 3 4 topnval TopSetR𝑡BaseR=TopOpenR
6 1 3 oppgbas BaseR=BaseO
7 1 4 oppgtset TopSetR=TopSetO
8 6 7 topnval TopSetR𝑡BaseR=TopOpenO
9 2 5 8 3eqtr2i J=TopOpenO