Theorem mapfoss

Description: The value of the set exponentiation ( B ^m A ) is a superset of the set of all functions from A onto B . (Contributed by AV, 7-Aug-2024)

	Ref	Expression
Assertion	mapfoss	|- { f | f : A -onto-> B } C_ ( B ^m A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- m e. _V
2		foeq1	|- ( f = m -> ( f : A -onto-> B <-> m : A -onto-> B ) )
3	1 2	elab	|- ( m e. { f | f : A -onto-> B } <-> m : A -onto-> B )
4		fof	|- ( m : A -onto-> B -> m : A --> B )
5		forn	|- ( m : A -onto-> B -> ran m = B )
6	1	rnex	|- ran m e. _V
7	5 6	eqeltrrdi	|- ( m : A -onto-> B -> B e. _V )
8		dmfex	|- ( ( m e. _V /\ m : A --> B ) -> A e. _V )
9	1 4 8	sylancr	|- ( m : A -onto-> B -> A e. _V )
10	7 9	elmapd	|- ( m : A -onto-> B -> ( m e. ( B ^m A ) <-> m : A --> B ) )
11	4 10	mpbird	|- ( m : A -onto-> B -> m e. ( B ^m A ) )
12	3 11	sylbi	|- ( m e. { f | f : A -onto-> B } -> m e. ( B ^m A ) )
13	12	ssriv	|- { f | f : A -onto-> B } C_ ( B ^m A )