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

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

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