Theorem gimfn

Description: The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Assertion	gimfn	$$⊢\mathrm{GrpIso}Fn\left(\mathrm{Grp}\times \mathrm{Grp}\right)$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		ovex	$$⊢s\mathrm{GrpHom}t\in \mathrm{V}$$
3	2	rabex	$$⊢\left\{g\in \left(s\mathrm{GrpHom}t\right)|g:{\mathrm{Base}}_s\underset{1-1\; onto}{⟶}{\mathrm{Base}}_t\right\}\in \mathrm{V}$$
4	1 3	fnmpoi	$$⊢\mathrm{GrpIso}Fn\left(\mathrm{Grp}\times \mathrm{Grp}\right)$$