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