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 = ( SymGrp ` A )
Assertion	idresperm	|- ( A e. V -> ( _I |` A ) e. ( Base ` G ) )

Proof

Step	Hyp	Ref	Expression
1		idresperm.g	|- G = ( SymGrp ` A )
2		f1oi	|- ( _I |` A ) : A -1-1-onto-> A
3		eqid	|- ( Base ` G ) = ( Base ` G )
4	1 3	elsymgbas	|- ( A e. V -> ( ( _I |` A ) e. ( Base ` G ) <-> ( _I |` A ) : A -1-1-onto-> A ) )
5	2 4	mpbiri	|- ( A e. V -> ( _I |` A ) e. ( Base ` G ) )