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 “ ( V ∖ 1o ) )
2 cnvimass ( GrpIso “ ( V ∖ 1o ) ) ⊆ dom GrpIso
3 gimfn GrpIso Fn ( Grp × Grp )
4 3 fndmi dom GrpIso = ( Grp × Grp )
5 2 4 sseqtri ( GrpIso “ ( V ∖ 1o ) ) ⊆ ( Grp × Grp )
6 1 5 eqsstri 𝑔 ⊆ ( Grp × Grp )
7 relxp Rel ( Grp × Grp )
8 relss ( ≃𝑔 ⊆ ( Grp × Grp ) → ( Rel ( Grp × Grp ) → Rel ≃𝑔 ) )
9 6 7 8 mp2 Rel ≃𝑔
10 gicsym ( 𝑥𝑔 𝑦𝑦𝑔 𝑥 )
11 gictr ( ( 𝑥𝑔 𝑦𝑦𝑔 𝑧 ) → 𝑥𝑔 𝑧 )
12 gicref ( 𝑥 ∈ Grp → 𝑥𝑔 𝑥 )
13 giclcl ( 𝑥𝑔 𝑥𝑥 ∈ Grp )
14 12 13 impbii ( 𝑥 ∈ Grp ↔ 𝑥𝑔 𝑥 )
15 9 10 11 14 iseri 𝑔 Er Grp