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

Metamath Proof Explorer

Theorem oppgtgp

Description: The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis oppgtmd.1 ⊢ 𝑂 = ( oppg ‘ 𝐺 )
Assertion oppgtgp ( 𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp )

Proof

Step Hyp Ref Expression
1 oppgtmd.1 ⊢ 𝑂 = ( oppg ‘ 𝐺 )
2 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
3 1 oppggrp ⊢ ( 𝐺 ∈ Grp → 𝑂 ∈ Grp )
4 2 3 syl ⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ Grp )
5 tgptmd ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
6 1 oppgtmd ⊢ ( 𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd )
7 5 6 syl ⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ TopMnd )
8 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
9 1 8 oppginv ⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) = ( invg ‘ 𝑂 ) )
10 2 9 syl ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) = ( invg ‘ 𝑂 ) )
11 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
12 11 8 tgpinv ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) )
13 10 12 eqeltrrd ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝑂 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) )
14 1 11 oppgtopn ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝑂 )
15 eqid ⊢ ( invg ‘ 𝑂 ) = ( invg ‘ 𝑂 )
16 14 15 istgp ⊢ ( 𝑂 ∈ TopGrp ↔ ( 𝑂 ∈ Grp ∧ 𝑂 ∈ TopMnd ∧ ( invg ‘ 𝑂 ) ∈ ( ( TopOpen ‘ 𝐺 ) Cn ( TopOpen ‘ 𝐺 ) ) ) )
17 4 7 13 16 syl3anbrc ⊢ ( 𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp )