Definition df-gim

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)

	Ref	Expression
Assertion	df-gim	|- GrpIso = ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgim	|- GrpIso
1		vs	|- s
2		cgrp	|- Grp
3		vt	|- t
4		vg	|- g
5	1	cv	|- s
6		cghm	|- GrpHom
7	3	cv	|- t
8	5 7 6	co	|- ( s GrpHom t )
9	4	cv	|- g
10		cbs	|- Base
11	5 10	cfv	|- ( Base ` s )
12	7 10	cfv	|- ( Base ` t )
13	11 12 9	wf1o	|- g : ( Base ` s ) -1-1-onto-> ( Base ` t )
14	13 4 8	crab	|- { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) }
15	1 3 2 2 14	cmpo	|- ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
16	0 15	wceq	|- GrpIso = ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )