This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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