Metamath Proof Explorer

Theorem oppggic

Description: Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypothesis oppggic.o 
|- O = ( oppG ` G )
Assertion oppggic 
|- ( G e. Grp -> G ~=g O )

Proof

Step Hyp Ref Expression
1 oppggic.o 
 |-  O = ( oppG ` G )
2 eqid 
 |-  ( invg ` G ) = ( invg ` G )
3 1 2 invoppggim 
 |-  ( G e. Grp -> ( invg ` G ) e. ( G GrpIso O ) )
4 brgici 
 |-  ( ( invg ` G ) e. ( G GrpIso O ) -> G ~=g O )
5 3 4 syl 
 |-  ( G e. Grp -> G ~=g O )