MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gim Structured version   Visualization version   GIF version

Definition df-gim 17467
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.)
Assertion
Ref Expression
df-gim GrpIso = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
Distinct variable group:   𝑔,𝑠,𝑡

Detailed syntax breakdown of Definition df-gim
StepHypRef Expression
1 cgim 17465 . 2 class GrpIso
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cgrp 17188 . . 3 class Grp
52cv 1473 . . . . . 6 class 𝑠
6 cbs 15638 . . . . . 6 class Base
75, 6cfv 5787 . . . . 5 class (Base‘𝑠)
83cv 1473 . . . . . 6 class 𝑡
98, 6cfv 5787 . . . . 5 class (Base‘𝑡)
10 vg . . . . . 6 setvar 𝑔
1110cv 1473 . . . . 5 class 𝑔
127, 9, 11wf1o 5786 . . . 4 wff 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)
13 cghm 17423 . . . . 5 class GrpHom
145, 8, 13co 6524 . . . 4 class (𝑠 GrpHom 𝑡)
1512, 10, 14crab 2896 . . 3 class {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)}
162, 3, 4, 4, 15cmpt2 6526 . 2 class (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
171, 16wceq 1474 1 wff GrpIso = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
Colors of variables: wff setvar class
This definition is referenced by:  gimfn  17469  isgim  17470
  Copyright terms: Public domain W3C validator