Definition df-gim 18398

Description: An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.)

Assertion

Ref	Expression
df-gim	⊢ GrpIso = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})

Distinct variable group:   𝑔,𝑠,𝑡

Detailed syntax breakdown of Definition df-gim

Step	Hyp	Ref	Expression
1		cgim 18396	. 2 class GrpIso
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cgrp 18102	. . 3 class Grp
5	2	cv 1532	. . . . . 6 class 𝑠
6		cbs 16482	. . . . . 6 class Base
7	5, 6	cfv 6354	. . . . 5 class (Base‘𝑠)
8	3	cv 1532	. . . . . 6 class 𝑡
9	8, 6	cfv 6354	. . . . 5 class (Base‘𝑡)
10		vg	. . . . . 6 setvar 𝑔
11	10	cv 1532	. . . . 5 class 𝑔
12	7, 9, 11	wf1o 6353	. . . 4 wff 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)
13		cghm 18354	. . . . 5 class GrpHom
14	5, 8, 13	co 7155	. . . 4 class (𝑠 GrpHom 𝑡)
15	12, 10, 14	crab 3142	. . 3 class {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}
16	2, 3, 4, 4, 15	cmpo 7157	. 2 class (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
17	1, 16	wceq 1533	1 wff GrpIso = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})

This definition is referenced by:  gimfn  18400  isgim  18401