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	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symgbasmap	$$⊢F\in B\to F\in \left(A^A\right)$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3	1 2	symgbasf	$$⊢F\in B\to F:A⟶A$$
4		simpr	$$⊢\left(F\in B\wedge F:A⟶A\right)\to F:A⟶A$$
5		dmfex	$$⊢\left(F\in B\wedge F:A⟶A\right)\to A\in \mathrm{V}$$
6	5 5	elmapd	$$⊢\left(F\in B\wedge F:A⟶A\right)\to \left(F\in \left(A^A\right)\leftrightarrow F:A⟶A\right)$$
7	4 6	mpbird	$$⊢\left(F\in B\wedge F:A⟶A\right)\to F\in \left(A^A\right)$$
8	3 7	mpdan	$$⊢F\in B\to F\in \left(A^A\right)$$