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=BaseG
cayley.h ⊢H=SymGrp⁡X
Assertion cayleyth ⊢G∈Grp→∃s∈SubGrp⁡H∃f∈GGrpHomH↾𝑠sf:X⟶1-1 ontos

Proof

Step Hyp Ref Expression
1 cayley.x ⊢X=BaseG
2 cayley.h ⊢H=SymGrp⁡X
3 eqid ⊢+G=+G
4 eqid ⊢g∈X⟼a∈X⟼g+Ga=g∈X⟼a∈X⟼g+Ga
5 eqid ⊢ran⁡g∈X⟼a∈X⟼g+Ga=ran⁡g∈X⟼a∈X⟼g+Ga
6 1 2 3 4 5 cayley ⊢G∈Grp→ran⁡g∈X⟼a∈X⟼g+Ga∈SubGrp⁡H∧g∈X⟼a∈X⟼g+Ga∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Ga∧g∈X⟼a∈X⟼g+Ga:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
7 6 simp1d ⊢G∈Grp→ran⁡g∈X⟼a∈X⟼g+Ga∈SubGrp⁡H
8 6 simp2d ⊢G∈Grp→g∈X⟼a∈X⟼g+Ga∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Ga
9 6 simp3d ⊢G∈Grp→g∈X⟼a∈X⟼g+Ga:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
10 f1oeq1 ⊢f=g∈X⟼a∈X⟼g+Ga→f:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga↔g∈X⟼a∈X⟼g+Ga:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
11 10 rspcev ⊢g∈X⟼a∈X⟼g+Ga∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Ga∧g∈X⟼a∈X⟼g+Ga:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga→∃f∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Gaf:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
12 8 9 11 syl2anc ⊢G∈Grp→∃f∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Gaf:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
13 oveq2 ⊢s=ran⁡g∈X⟼a∈X⟼g+Ga→H↾𝑠s=H↾𝑠ran⁡g∈X⟼a∈X⟼g+Ga
14 13 oveq2d ⊢s=ran⁡g∈X⟼a∈X⟼g+Ga→GGrpHomH↾𝑠s=GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Ga
15 f1oeq3 ⊢s=ran⁡g∈X⟼a∈X⟼g+Ga→f:X⟶1-1 ontos↔f:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
16 14 15 rexeqbidv ⊢s=ran⁡g∈X⟼a∈X⟼g+Ga→∃f∈GGrpHomH↾𝑠sf:X⟶1-1 ontos↔∃f∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Gaf:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga
17 16 rspcev ⊢ran⁡g∈X⟼a∈X⟼g+Ga∈SubGrp⁡H∧∃f∈GGrpHomH↾𝑠ran⁡g∈X⟼a∈X⟼g+Gaf:X⟶1-1 ontoran⁡g∈X⟼a∈X⟼g+Ga→∃s∈SubGrp⁡H∃f∈GGrpHomH↾𝑠sf:X⟶1-1 ontos
18 7 12 17 syl2anc ⊢G∈Grp→∃s∈SubGrp⁡H∃f∈GGrpHomH↾𝑠sf:X⟶1-1 ontos