Metamath Proof Explorer


Theorem oppgtopn

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

Ref Expression
Hypotheses oppgbas.1
|- O = ( oppG ` R )
oppgtopn.2
|- J = ( TopOpen ` R )
Assertion oppgtopn
|- J = ( TopOpen ` O )

Proof

Step Hyp Ref Expression
1 oppgbas.1
 |-  O = ( oppG ` R )
2 oppgtopn.2
 |-  J = ( TopOpen ` R )
3 eqid
 |-  ( Base ` R ) = ( Base ` R )
4 eqid
 |-  ( TopSet ` R ) = ( TopSet ` R )
5 3 4 topnval
 |-  ( ( TopSet ` R ) |`t ( Base ` R ) ) = ( TopOpen ` R )
6 1 3 oppgbas
 |-  ( Base ` R ) = ( Base ` O )
7 1 4 oppgtset
 |-  ( TopSet ` R ) = ( TopSet ` O )
8 6 7 topnval
 |-  ( ( TopSet ` R ) |`t ( Base ` R ) ) = ( TopOpen ` O )
9 2 5 8 3eqtr2i
 |-  J = ( TopOpen ` O )