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	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion	idresperm	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		idresperm.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		f1oi	⊢ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴
3		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
4	1 3	elsymgbas	⊢ ( 𝐴 ∈ 𝑉 → ( ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) ↔ ( I ↾ 𝐴 ) : 𝐴 –1-1-onto→ 𝐴 ) )
5	2 4	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ ( Base ‘ 𝐺 ) )