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	$$⊢\mathrm{GrpIso}=\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g\in \left(s\mathrm{GrpHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgim	$$class\mathrm{GrpIso}$$
1		vs	$$setvars$$
2		cgrp	$$class\mathrm{Grp}$$
3		vt	$$setvart$$
4		vg	$$setvarg$$
5	1	cv	$$setvars$$
6		cghm	$$class\mathrm{GrpHom}$$
7	3	cv	$$setvart$$
8	5 7 6	co	$$class\left(s\mathrm{GrpHom}t\right)$$
9	4	cv	$$setvarg$$
10		cbs	$$class\mathrm{Base}$$
11	5 10	cfv	$$class{\mathrm{Base}}_s$$
12	7 10	cfv	$$class{\mathrm{Base}}_t$$
13	11 12 9	wf1o	$$wffg:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t$$
14	13 4 8	crab	$$class\left\{g\in \left(s\mathrm{GrpHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}$$
15	1 3 2 2 14	cmpo	$$class\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g\in \left(s\mathrm{GrpHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{GrpIso}=\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g\in \left(s\mathrm{GrpHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\right)$$