Definition df-gim 17701

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 = ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )

Distinct variable group:   g, s, t

Detailed syntax breakdown of Definition df-gim

Step	Hyp	Ref	Expression
1		cgim 17699	. 2 class GrpIso
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cgrp 17422	. . 3 class Grp
5	2	cv 1482	. . . . . 6 class s
6		cbs 15857	. . . . . 6 class Base
7	5, 6	cfv 5888	. . . . 5 class ( Base ` s )
8	3	cv 1482	. . . . . 6 class t
9	8, 6	cfv 5888	. . . . 5 class ( Base ` t )
10		vg	. . . . . 6 setvar g
11	10	cv 1482	. . . . 5 class g
12	7, 9, 11	wf1o 5887	. . . 4 wff g : ( Base ` s ) -1-1-onto-> ( Base ` t )
13		cghm 17657	. . . . 5 class GrpHom
14	5, 8, 13	co 6650	. . . 4 class ( s GrpHom t )
15	12, 10, 14	crab 2916	. . 3 class { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) }
16	2, 3, 4, 4, 15	cmpt2 6652	. 2 class ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
17	1, 16	wceq 1483	1 wff GrpIso = ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )

This definition is referenced by:  gimfn  17703  isgim  17704