Theorem symgbasmap

Description: A permutation (element of the symmetric group) is a mapping (or set exponentiation) from a set into itself. (Contributed by AV, 30-Mar-2024)

	Ref	Expression
Hypotheses	symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
	symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	symgbasmap	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( 𝐴 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2		symgbas.2	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	1 2	symgbasf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐴 )
4		simpr	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐴 )
5		dmfex	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐴 ) → 𝐴 ∈ V )
6	5 5	elmapd	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐴 ) → ( 𝐹 ∈ ( 𝐴 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐴 ) )
7	4 6	mpbird	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐴 ) → 𝐹 ∈ ( 𝐴 ↑m 𝐴 ) )
8	3 7	mpdan	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( 𝐴 ↑m 𝐴 ) )