Theorem idressubgsymg

Description: The singleton containing only the identity function restricted to a set is a subgroup of the symmetric group of this set. (Contributed by AV, 17-Mar-2019)

	Ref	Expression
Hypothesis	idressubgsymg.g	|- G = ( SymGrp ` A )
Assertion	idressubgsymg	|- ( A e. V -> { ( _I |` A ) } e. ( SubGrp ` G ) )

Proof

Step	Hyp	Ref	Expression
1		idressubgsymg.g	|- G = ( SymGrp ` A )
2	1	symgid	|- ( A e. V -> ( _I |` A ) = ( 0g ` G ) )
3	2	sneqd	|- ( A e. V -> { ( _I |` A ) } = { ( 0g ` G ) } )
4	1	symggrp	|- ( A e. V -> G e. Grp )
5		eqid	|- ( 0g ` G ) = ( 0g ` G )
6	5	0subg	|- ( G e. Grp -> { ( 0g ` G ) } e. ( SubGrp ` G ) )
7	4 6	syl	|- ( A e. V -> { ( 0g ` G ) } e. ( SubGrp ` G ) )
8	3 7	eqeltrd	|- ( A e. V -> { ( _I |` A ) } e. ( SubGrp ` G ) )