This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = TopOpen ⁡ R
Assertion oppgtopn ⊢ J = TopOpen ⁡ O

Proof

Step Hyp Ref Expression
1 oppgbas.1 ⊢ O = opp 𝑔 ⁡ 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 ↾ 𝑡 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 ↾ 𝑡 Base R = TopOpen ⁡ O
9 2 5 8 3eqtr2i ⊢ J = TopOpen ⁡ O