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 e. Grp -> E. s e. ( SubGrp ` H ) E. f e. ( G GrpHom ( H |`s 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 ) = ( +g ` G )
4 eqid 
 |-  ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) = ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) )
5 eqid 
 |-  ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) = ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) )
6 1 2 3 4 5 cayley 
 |-  ( G e. Grp -> ( ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) e. ( SubGrp ` H ) /\ ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) /\ ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) )
7 6 simp1d 
 |-  ( G e. Grp -> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) e. ( SubGrp ` H ) )
8 6 simp2d 
 |-  ( G e. Grp -> ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) )
9 6 simp3d 
 |-  ( G e. Grp -> ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) )
10 f1oeq1 
 |-  ( f = ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) -> ( f : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) <-> ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) )
11 10 rspcev 
 |-  ( ( ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) /\ ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) -> E. f e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) f : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) )
12 8 9 11 syl2anc 
 |-  ( G e. Grp -> E. f e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) f : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) )
13 oveq2 
 |-  ( s = ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) -> ( H |`s s ) = ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) )
14 13 oveq2d 
 |-  ( s = ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) -> ( G GrpHom ( H |`s s ) ) = ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) )
15 f1oeq3 
 |-  ( s = ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) -> ( f : X -1-1-onto-> s <-> f : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) )
16 14 15 rexeqbidv 
 |-  ( s = ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) -> ( E. f e. ( G GrpHom ( H |`s s ) ) f : X -1-1-onto-> s <-> E. f e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) f : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) )
17 16 rspcev 
 |-  ( ( ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) e. ( SubGrp ` H ) /\ E. f e. ( G GrpHom ( H |`s ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) ) f : X -1-1-onto-> ran ( g e. X |-> ( a e. X |-> ( g ( +g ` G ) a ) ) ) ) -> E. s e. ( SubGrp ` H ) E. f e. ( G GrpHom ( H |`s s ) ) f : X -1-1-onto-> s )
18 7 12 17 syl2anc 
 |-  ( G e. Grp -> E. s e. ( SubGrp ` H ) E. f e. ( G GrpHom ( H |`s s ) ) f : X -1-1-onto-> s )