Theorem idrespermg

Description: The structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation (constructed by (structure) restricting the symmetric group to that singleton) is a permutation group (group consisting of permutations). (Contributed by AV, 17-Mar-2019)

	Ref	Expression
Hypotheses	idressubgsymg.g	|- G = ( SymGrp ` A )
	idrespermg.e	|- E = ( G |`s { ( _I |` A ) } )
Assertion	idrespermg	|- ( A e. V -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )

Proof

Step	Hyp	Ref	Expression
1		idressubgsymg.g	|- G = ( SymGrp ` A )
2		idrespermg.e	|- E = ( G |`s { ( _I |` A ) } )
3	1	idressubgsymg	|- ( A e. V -> { ( _I |` A ) } e. ( SubGrp ` G ) )
4		eqid	|- ( Base ` G ) = ( Base ` G )
5	1 4	pgrpsubgsymgbi	|- ( A e. V -> ( { ( _I |` A ) } e. ( SubGrp ` G ) <-> ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) ) )
6		snex	|- { ( _I |` A ) } e. _V
7	2 4	ressbas	|- ( { ( _I |` A ) } e. _V -> ( { ( _I |` A ) } i^i ( Base ` G ) ) = ( Base ` E ) )
8	6 7	mp1i	|- ( A e. V -> ( { ( _I |` A ) } i^i ( Base ` G ) ) = ( Base ` E ) )
9		inss2	|- ( { ( _I |` A ) } i^i ( Base ` G ) ) C_ ( Base ` G )
10	8 9	eqsstrrdi	|- ( A e. V -> ( Base ` E ) C_ ( Base ` G ) )
11	2	eqcomi	|- ( G |`s { ( _I |` A ) } ) = E
12	11	eleq1i	|- ( ( G |`s { ( _I |` A ) } ) e. Grp <-> E e. Grp )
13	12	biimpi	|- ( ( G |`s { ( _I |` A ) } ) e. Grp -> E e. Grp )
14	13	adantl	|- ( ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) -> E e. Grp )
15	10 14	anim12ci	|- ( ( A e. V /\ ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) ) -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )
16	15	ex	|- ( A e. V -> ( ( { ( _I |` A ) } C_ ( Base ` G ) /\ ( G |`s { ( _I |` A ) } ) e. Grp ) -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) ) )
17	5 16	sylbid	|- ( A e. V -> ( { ( _I |` A ) } e. ( SubGrp ` G ) -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) ) )
18	3 17	mpd	|- ( A e. V -> ( E e. Grp /\ ( Base ` E ) C_ ( Base ` G ) ) )