gicsym

Description: Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016)

		Ref	Expression
	Assertion	gicsym	$⊢ R ≃_{𝑔} S \to S ≃_{𝑔} R$

Step	Hyp	Ref	Expression
1		brgic	$⊢ R ≃_{𝑔} S \leftrightarrow R GrpIso S \neq \emptyset$
2		n0	$⊢ R GrpIso S \neq \emptyset \leftrightarrow \exists f f \in (R GrpIso S)$
3		gimcnv	$⊢ f \in (R GrpIso S) \to f^{-1} \in (S GrpIso R)$
4		brgici	$⊢ f^{-1} \in (S GrpIso R) \to S ≃_{𝑔} R$
5	3 4	syl	$⊢ f \in (R GrpIso S) \to S ≃_{𝑔} R$
6	5	exlimiv	$⊢ \exists f f \in (R GrpIso S) \to S ≃_{𝑔} R$
7	2 6	sylbi	$⊢ R GrpIso S \neq \emptyset \to S ≃_{𝑔} R$
8	1 7	sylbi	$⊢ R ≃_{𝑔} S \to S ≃_{𝑔} R$

Metamath Proof Explorer