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

Metamath Proof Explorer

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 = s ∈ Grp , t ∈ Grp ⟼ g ∈ s GrpHom t | g : Base s ⟶ 1-1 onto Base t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgim class GrpIso
1 vs setvar s
2 cgrp class Grp
3 vt setvar t
4 vg setvar g
5 1 cv setvar s
6 cghm class GrpHom
7 3 cv setvar t
8 5 7 6 co class s GrpHom t
9 4 cv setvar g
10 cbs class Base
11 5 10 cfv class Base s
12 7 10 cfv class Base t
13 11 12 9 wf1o wff g : Base s ⟶ 1-1 onto Base t
14 13 4 8 crab class g ∈ s GrpHom t | g : Base s ⟶ 1-1 onto Base t
15 1 3 2 2 14 cmpo class s ∈ Grp , t ∈ Grp ⟼ g ∈ s GrpHom t | g : Base s ⟶ 1-1 onto Base t
16 0 15 wceq wff GrpIso = s ∈ Grp , t ∈ Grp ⟼ g ∈ s GrpHom t | g : Base s ⟶ 1-1 onto Base t