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 = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symgbasmap	|- ( F e. B -> F e. ( A ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3	1 2	symgbasf	|- ( F e. B -> F : A --> A )
4		simpr	|- ( ( F e. B /\ F : A --> A ) -> F : A --> A )
5		dmfex	|- ( ( F e. B /\ F : A --> A ) -> A e. _V )
6	5 5	elmapd	|- ( ( F e. B /\ F : A --> A ) -> ( F e. ( A ^m A ) <-> F : A --> A ) )
7	4 6	mpbird	|- ( ( F e. B /\ F : A --> A ) -> F e. ( A ^m A ) )
8	3 7	mpdan	|- ( F e. B -> F e. ( A ^m A ) )