Theorem idresperm

Description: The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019)

	Ref	Expression
Hypothesis	idresperm.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
Assertion	idresperm	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		idresperm.g	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4	1 3	elsymgbas	$$⊢A\in V\to \left({\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G\leftrightarrow \left({\mathrm{I}\upharpoonright }_A\right):A\underset{1-1\; onto}{⟶}A\right)$$
5	2 4	mpbiri	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in {\mathrm{Base}}_G$$