Metamath Proof Explorer

Theorem pgrpsubgsymgbi

Description: Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019)

Ref Expression
Hypotheses pgrpsubgsymgbi.g 
|- G = ( SymGrp ` A )
pgrpsubgsymgbi.b 
|- B = ( Base ` G )
Assertion pgrpsubgsymgbi 
|- ( A e. V -> ( P e. ( SubGrp ` G ) <-> ( P C_ B /\ ( G |`s P ) e. Grp ) ) )

Proof

Step Hyp Ref Expression
1 pgrpsubgsymgbi.g 
 |-  G = ( SymGrp ` A )
2 pgrpsubgsymgbi.b 
 |-  B = ( Base ` G )
3 2 issubg 
 |-  ( P e. ( SubGrp ` G ) <-> ( G e. Grp /\ P C_ B /\ ( G |`s P ) e. Grp ) )
4 3anass 
 |-  ( ( G e. Grp /\ P C_ B /\ ( G |`s P ) e. Grp ) <-> ( G e. Grp /\ ( P C_ B /\ ( G |`s P ) e. Grp ) ) )
5 3 4 bitri 
 |-  ( P e. ( SubGrp ` G ) <-> ( G e. Grp /\ ( P C_ B /\ ( G |`s P ) e. Grp ) ) )
6 1 symggrp 
 |-  ( A e. V -> G e. Grp )
7 ibar 
 |-  ( G e. Grp -> ( ( P C_ B /\ ( G |`s P ) e. Grp ) <-> ( G e. Grp /\ ( P C_ B /\ ( G |`s P ) e. Grp ) ) ) )
8 7 bicomd 
 |-  ( G e. Grp -> ( ( G e. Grp /\ ( P C_ B /\ ( G |`s P ) e. Grp ) ) <-> ( P C_ B /\ ( G |`s P ) e. Grp ) ) )
9 6 8 syl 
 |-  ( A e. V -> ( ( G e. Grp /\ ( P C_ B /\ ( G |`s P ) e. Grp ) ) <-> ( P C_ B /\ ( G |`s P ) e. Grp ) ) )
10 5 9 bitrid 
 |-  ( A e. V -> ( P e. ( SubGrp ` G ) <-> ( P C_ B /\ ( G |`s P ) e. Grp ) ) )