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 
|- O = ( oppG ` G )
Assertion oppgtgp 
|- ( G e. TopGrp -> O e. TopGrp )

Proof

Step Hyp Ref Expression
1 oppgtmd.1 
 |-  O = ( oppG ` G )
2 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
3 1 oppggrp 
 |-  ( G e. Grp -> O e. Grp )
4 2 3 syl 
 |-  ( G e. TopGrp -> O e. Grp )
5 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
6 1 oppgtmd 
 |-  ( G e. TopMnd -> O e. TopMnd )
7 5 6 syl 
 |-  ( G e. TopGrp -> O e. TopMnd )
8 eqid 
 |-  ( invg ` G ) = ( invg ` G )
9 1 8 oppginv 
 |-  ( G e. Grp -> ( invg ` G ) = ( invg ` O ) )
10 2 9 syl 
 |-  ( G e. TopGrp -> ( invg ` G ) = ( invg ` O ) )
11 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
12 11 8 tgpinv 
 |-  ( G e. TopGrp -> ( invg ` G ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
13 10 12 eqeltrrd 
 |-  ( G e. TopGrp -> ( invg ` O ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) )
14 1 11 oppgtopn 
 |-  ( TopOpen ` G ) = ( TopOpen ` O )
15 eqid 
 |-  ( invg ` O ) = ( invg ` O )
16 14 15 istgp 
 |-  ( O e. TopGrp <-> ( O e. Grp /\ O e. TopMnd /\ ( invg ` O ) e. ( ( TopOpen ` G ) Cn ( TopOpen ` G ) ) ) )
17 4 7 13 16 syl3anbrc 
 |-  ( G e. TopGrp -> O e. TopGrp )