Theorem gimfn

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

	Ref	Expression
Assertion	gimfn	⊢ GrpIso Fn ( Grp × Grp )

Proof

Step	Hyp	Ref	Expression
1		df-gim	⊢ GrpIso = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } )
2		ovex	⊢ ( 𝑠 GrpHom 𝑡 ) ∈ V
3	2	rabex	⊢ { 𝑔 ∈ ( 𝑠 GrpHom 𝑡 ) ∣ 𝑔 : ( Base ‘ 𝑠 ) –1-1-onto→ ( Base ‘ 𝑡 ) } ∈ V
4	1 3	fnmpoi	⊢ GrpIso Fn ( Grp × Grp )