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 𝑔 Er Grp

Proof

Step Hyp Ref Expression
1 df-gic 𝑔 = GrpIso -1 V 1 𝑜
2 cnvimass GrpIso -1 V 1 𝑜 dom GrpIso
3 gimfn GrpIso Fn Grp × Grp
4 fndm GrpIso Fn Grp × Grp dom GrpIso = Grp × Grp
5 3 4 ax-mp dom GrpIso = Grp × Grp
6 2 5 sseqtri GrpIso -1 V 1 𝑜 Grp × Grp
7 1 6 eqsstri 𝑔 Grp × Grp
8 relxp Rel Grp × Grp
9 relss 𝑔 Grp × Grp Rel Grp × Grp Rel 𝑔
10 7 8 9 mp2 Rel 𝑔
11 gicsym x 𝑔 y y 𝑔 x
12 gictr x 𝑔 y y 𝑔 z x 𝑔 z
13 gicref x Grp x 𝑔 x
14 giclcl x 𝑔 x x Grp
15 13 14 impbii x Grp x 𝑔 x
16 10 11 12 15 iseri 𝑔 Er Grp