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 = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgim	⊢ GrpIso
1		vs	⊢ 𝑠
2		cgrp	⊢ Grp
3		vt	⊢ 𝑡
4		vg	⊢ 𝑔
5	1	cv	⊢ 𝑠
6		cghm	⊢ GrpHom
7	3	cv	⊢ 𝑡
8	5 7 6	co	⊢ ( 𝑠 GrpHom 𝑡 )
9	4	cv	⊢ 𝑔
10		cbs	⊢ Base
11	5 10	cfv	⊢ ( Base ‘ 𝑠 )
12	7 10	cfv	⊢ ( Base ‘ 𝑡 )
13	11 12 9	wf1o	⊢ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 )
14	13 4 8	crab	⊢ { 𝑔 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) }
15	1 3 2 2 14	cmpo	⊢ ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )
16	0 15	wceq	⊢ GrpIso = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )