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={opp}_{𝑔}\left(G\right)$$
Assertion	oppggic	$$⊢G\in \mathrm{Grp}\to G{\simeq }_{𝑔}O$$

Proof

Step	Hyp	Ref	Expression
1		oppggic.o	$$⊢O={opp}_{𝑔}\left(G\right)$$
2		eqid	$$⊢{inv}_g\left(G\right)={inv}_g\left(G\right)$$
3	1 2	invoppggim	$$⊢G\in \mathrm{Grp}\to {inv}_g\left(G\right)\in \left(G\mathrm{GrpIso}O\right)$$
4		brgici	$$⊢{inv}_g\left(G\right)\in \left(G\mathrm{GrpIso}O\right)\to G{\simeq }_{𝑔}O$$
5	3 4	syl	$$⊢G\in \mathrm{Grp}\to G{\simeq }_{𝑔}O$$