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=\mathrm{SymGrp}\left(A\right)$$
Assertion	idressubgsymg	$$⊢A\in V\to \left\{{\mathrm{I}\upharpoonright }_A\right\}\in \mathrm{SubGrp}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		idressubgsymg.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2	1	symgid	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A=0_G$$
3	2	sneqd	$$⊢A\in V\to \left\{{\mathrm{I}\upharpoonright }_A\right\}=\left\{0_G\right\}$$
4	1	symggrp	$$⊢A\in V\to G\in \mathrm{Grp}$$
5		eqid	$$⊢0_G=0_G$$
6	5	0subg	$$⊢G\in \mathrm{Grp}\to \left\{0_G\right\}\in \mathrm{SubGrp}\left(G\right)$$
7	4 6	syl	$$⊢A\in V\to \left\{0_G\right\}\in \mathrm{SubGrp}\left(G\right)$$
8	3 7	eqeltrd	$$⊢A\in V\to \left\{{\mathrm{I}\upharpoonright }_A\right\}\in \mathrm{SubGrp}\left(G\right)$$