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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion	idressubgsymg	⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		idressubgsymg.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2	1	symgid	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) = ( 0g ‘ 𝐺 ) )
3	2	sneqd	⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } = { ( 0g ‘ 𝐺 ) } )
4	1	symggrp	⊢ ( 𝐴 ∈ 𝑉 → 𝐺 ∈ Grp )
5		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6	5	0subg	⊢ ( 𝐺 ∈ Grp → { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) )
7	4 6	syl	⊢ ( 𝐴 ∈ 𝑉 → { ( 0g ‘ 𝐺 ) } ∈ ( SubGrp ‘ 𝐺 ) )
8	3 7	eqeltrd	⊢ ( 𝐴 ∈ 𝑉 → { ( I ↾ 𝐴 ) } ∈ ( SubGrp ‘ 𝐺 ) )