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	$$⊢\left\{f|f:A\underset{onto}{⟶}B\right\}\subseteq B^A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢m\in \mathrm{V}$$
2		foeq1	$$⊢f=m\to \left(f:A\underset{onto}{⟶}B\leftrightarrow m:A\underset{onto}{⟶}B\right)$$
3	1 2	elab	$$⊢m\in \left\{f|f:A\underset{onto}{⟶}B\right\}\leftrightarrow m:A\underset{onto}{⟶}B$$
4		fof	$$⊢m:A\underset{onto}{⟶}B\to m:A⟶B$$
5		forn	$$⊢m:A\underset{onto}{⟶}B\to \mathrm{ran}m=B$$
6	1	rnex	$$⊢\mathrm{ran}m\in \mathrm{V}$$
7	5 6	eqeltrrdi	$$⊢m:A\underset{onto}{⟶}B\to B\in \mathrm{V}$$
8		dmfex	$$⊢\left(m\in \mathrm{V}\wedge m:A⟶B\right)\to A\in \mathrm{V}$$
9	1 4 8	sylancr	$$⊢m:A\underset{onto}{⟶}B\to A\in \mathrm{V}$$
10	7 9	elmapd	$$⊢m:A\underset{onto}{⟶}B\to \left(m\in \left(B^A\right)\leftrightarrow m:A⟶B\right)$$
11	4 10	mpbird	$$⊢m:A\underset{onto}{⟶}B\to m\in \left(B^A\right)$$
12	3 11	sylbi	$$⊢m\in \left\{f|f:A\underset{onto}{⟶}B\right\}\to m\in \left(B^A\right)$$
13	12	ssriv	$$⊢\left\{f|f:A\underset{onto}{⟶}B\right\}\subseteq B^A$$