Metamath Proof Explorer


Theorem cayleyth

Description: Cayley's Theorem (existence version): every group G is isomorphic to a subgroup of the symmetric group on the underlying set of G . (For any group G there exists an isomorphism f between G and a subgroup h of the symmetric group on the underlying set of G .) See also Theorem 3.15 in Rotman p. 42. (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cayley.x X = Base G
cayley.h H = SymGrp X
Assertion cayleyth G Grp s SubGrp H f G GrpHom H 𝑠 s f : X 1-1 onto s

Proof

Step Hyp Ref Expression
1 cayley.x X = Base G
2 cayley.h H = SymGrp X
3 eqid + G = + G
4 eqid g X a X g + G a = g X a X g + G a
5 eqid ran g X a X g + G a = ran g X a X g + G a
6 1 2 3 4 5 cayley G Grp ran g X a X g + G a SubGrp H g X a X g + G a G GrpHom H 𝑠 ran g X a X g + G a g X a X g + G a : X 1-1 onto ran g X a X g + G a
7 6 simp1d G Grp ran g X a X g + G a SubGrp H
8 6 simp2d G Grp g X a X g + G a G GrpHom H 𝑠 ran g X a X g + G a
9 6 simp3d G Grp g X a X g + G a : X 1-1 onto ran g X a X g + G a
10 f1oeq1 f = g X a X g + G a f : X 1-1 onto ran g X a X g + G a g X a X g + G a : X 1-1 onto ran g X a X g + G a
11 10 rspcev g X a X g + G a G GrpHom H 𝑠 ran g X a X g + G a g X a X g + G a : X 1-1 onto ran g X a X g + G a f G GrpHom H 𝑠 ran g X a X g + G a f : X 1-1 onto ran g X a X g + G a
12 8 9 11 syl2anc G Grp f G GrpHom H 𝑠 ran g X a X g + G a f : X 1-1 onto ran g X a X g + G a
13 oveq2 s = ran g X a X g + G a H 𝑠 s = H 𝑠 ran g X a X g + G a
14 13 oveq2d s = ran g X a X g + G a G GrpHom H 𝑠 s = G GrpHom H 𝑠 ran g X a X g + G a
15 f1oeq3 s = ran g X a X g + G a f : X 1-1 onto s f : X 1-1 onto ran g X a X g + G a
16 14 15 rexeqbidv s = ran g X a X g + G a f G GrpHom H 𝑠 s f : X 1-1 onto s f G GrpHom H 𝑠 ran g X a X g + G a f : X 1-1 onto ran g X a X g + G a
17 16 rspcev ran g X a X g + G a SubGrp H f G GrpHom H 𝑠 ran g X a X g + G a f : X 1-1 onto ran g X a X g + G a s SubGrp H f G GrpHom H 𝑠 s f : X 1-1 onto s
18 7 12 17 syl2anc G Grp s SubGrp H f G GrpHom H 𝑠 s f : X 1-1 onto s