Theorem 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	$$⊢{\simeq }_{𝑔}\mathrm{Er}\mathrm{Grp}$$

Proof

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