Metamath Proof Explorer


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 ‘ 𝐺 ) )