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 
|- ~=g Er Grp

Proof

Step Hyp Ref Expression
1 df-gic 
 |-  ~=g = ( `' GrpIso " ( _V \ 1o ) )
2 cnvimass 
 |-  ( `' GrpIso " ( _V \ 1o ) ) C_ dom GrpIso
3 gimfn 
 |-  GrpIso Fn ( Grp X. Grp )
4 3 fndmi 
 |-  dom GrpIso = ( Grp X. Grp )
5 2 4 sseqtri 
 |-  ( `' GrpIso " ( _V \ 1o ) ) C_ ( Grp X. Grp )
6 1 5 eqsstri 
 |-  ~=g C_ ( Grp X. Grp )
7 relxp 
 |-  Rel ( Grp X. Grp )
8 relss 
 |-  ( ~=g C_ ( Grp X. Grp ) -> ( Rel ( Grp X. Grp ) -> Rel ~=g ) )
9 6 7 8 mp2 
 |-  Rel ~=g
10 gicsym 
 |-  ( x ~=g y -> y ~=g x )
11 gictr 
 |-  ( ( x ~=g y /\ y ~=g z ) -> x ~=g z )
12 gicref 
 |-  ( x e. Grp -> x ~=g x )
13 giclcl 
 |-  ( x ~=g x -> x e. Grp )
14 12 13 impbii 
 |-  ( x e. Grp <-> x ~=g x )
15 9 10 11 14 iseri 
 |-  ~=g Er Grp