# Metamath Proof Explorer

## 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}×\mathrm{Grp}\right)$
4 fndm ${⊢}\mathrm{GrpIso}Fn\left(\mathrm{Grp}×\mathrm{Grp}\right)\to \mathrm{dom}\mathrm{GrpIso}=\mathrm{Grp}×\mathrm{Grp}$
5 3 4 ax-mp ${⊢}\mathrm{dom}\mathrm{GrpIso}=\mathrm{Grp}×\mathrm{Grp}$
6 2 5 sseqtri ${⊢}{\mathrm{GrpIso}}^{-1}\left[\mathrm{V}\setminus {1}_{𝑜}\right]\subseteq \mathrm{Grp}×\mathrm{Grp}$
7 1 6 eqsstri ${⊢}{\simeq }_{𝑔}\subseteq \mathrm{Grp}×\mathrm{Grp}$
8 relxp ${⊢}\mathrm{Rel}\left(\mathrm{Grp}×\mathrm{Grp}\right)$
9 relss ${⊢}{\simeq }_{𝑔}\subseteq \mathrm{Grp}×\mathrm{Grp}\to \left(\mathrm{Rel}\left(\mathrm{Grp}×\mathrm{Grp}\right)\to \mathrm{Rel}{\simeq }_{𝑔}\right)$
10 7 8 9 mp2 ${⊢}\mathrm{Rel}{\simeq }_{𝑔}$
11 gicsym ${⊢}{x}{\simeq }_{𝑔}{y}\to {y}{\simeq }_{𝑔}{x}$
12 gictr ${⊢}\left({x}{\simeq }_{𝑔}{y}\wedge {y}{\simeq }_{𝑔}{z}\right)\to {x}{\simeq }_{𝑔}{z}$
13 gicref ${⊢}{x}\in \mathrm{Grp}\to {x}{\simeq }_{𝑔}{x}$
14 giclcl ${⊢}{x}{\simeq }_{𝑔}{x}\to {x}\in \mathrm{Grp}$
15 13 14 impbii ${⊢}{x}\in \mathrm{Grp}↔{x}{\simeq }_{𝑔}{x}$
16 10 11 12 15 iseri ${⊢}{\simeq }_{𝑔}\mathrm{Er}\mathrm{Grp}$