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