gicer

Description: Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 1-May-2021)

		Ref	Expression
	Assertion	gicer	$⊢ ≃_{𝑔} Er Grp$

Step	Hyp	Ref	Expression
1		df-gic	$⊢ ≃_{𝑔} = {GrpIso}^{-1} [V ∖ 1_{𝑜}]$
2		cnvimass	$⊢ {GrpIso}^{-1} [V ∖ 1_{𝑜}] \subseteq dom GrpIso$
3		gimfn	$⊢ GrpIso Fn (Grp \times Grp)$
4	3	fndmi	$⊢ dom GrpIso = Grp \times Grp$
5	2 4	sseqtri	$⊢ {GrpIso}^{-1} [V ∖ 1_{𝑜}] \subseteq Grp \times Grp$
6	1 5	eqsstri	$⊢ ≃_{𝑔} \subseteq Grp \times Grp$
7		relxp	$⊢ Rel (Grp \times Grp)$
8		relss	$⊢ ≃_{𝑔} \subseteq Grp \times Grp \to (Rel (Grp \times Grp) \to Rel ≃_{𝑔})$
9	6 7 8	mp2	$⊢ Rel ≃_{𝑔}$
10		gicsym	$⊢ x ≃_{𝑔} y \to y ≃_{𝑔} x$
11		gictr	$⊢ (x ≃_{𝑔} y \land y ≃_{𝑔} z) \to x ≃_{𝑔} z$
12		gicref	$⊢ x \in Grp \to x ≃_{𝑔} x$
13		giclcl	$⊢ x ≃_{𝑔} x \to x \in Grp$
14	12 13	impbii	$⊢ x \in Grp \leftrightarrow x ≃_{𝑔} x$
15	9 10 11 14	iseri	$⊢ ≃_{𝑔} Er Grp$

Metamath Proof Explorer