Database
BASIC ALGEBRAIC STRUCTURES
Groups
Isomorphisms of groups
brgic
Next ⟩
brgici
Metamath Proof Explorer
Ascii
Unicode
Theorem
brgic
Description:
The relation "is isomorphic to" for groups.
(Contributed by
Stefan O'Rear
, 25-Jan-2015)
Ref
Expression
Assertion
brgic
⊢
R
≃
𝑔
S
↔
R
GrpIso
S
≠
∅
Proof
Step
Hyp
Ref
Expression
1
df-gic
⊢
≃
𝑔
=
GrpIso
-1
V
∖
1
𝑜
2
gimfn
⊢
GrpIso
Fn
Grp
×
Grp
3
1
2
brwitnlem
⊢
R
≃
𝑔
S
↔
R
GrpIso
S
≠
∅