This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = s ∈ Grp , t ∈ Grp ⟼ g ∈ s GrpHom t | g : Base s ⟶ 1-1 onto Base t
2 ovex ⊢ s GrpHom t ∈ V
3 2 rabex ⊢ g ∈ s GrpHom t | g : Base s ⟶ 1-1 onto Base t ∈ V
4 1 3 fnmpoi ⊢ GrpIso Fn Grp × Grp