Theorem mapssfset

Description: The value of the set exponentiation ( B ^m A ) is a subset of the class of functions from A to B . (Contributed by AV, 10-Aug-2024)

	Ref	Expression
Assertion	mapssfset	$$⊢B^A\subseteq \left\{f|f:A⟶B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mapfset	$$⊢B\in \mathrm{V}\to \left\{f|f:A⟶B\right\}=B^A$$
2		eqimss2	$$⊢\left\{f|f:A⟶B\right\}=B^A\to B^A\subseteq \left\{f|f:A⟶B\right\}$$
3	1 2	syl	$$⊢B\in \mathrm{V}\to B^A\subseteq \left\{f|f:A⟶B\right\}$$
4		reldmmap	$$⊢\mathrm{Rel}\mathrm{dom}{\uparrow }_{𝑚}$$
5	4	ovprc1	$$⊢\neg B\in \mathrm{V}\to B^A=\varnothing$$
6		0ss	$$⊢\varnothing \subseteq \left\{f|f:A⟶B\right\}$$
7	5 6	eqsstrdi	$$⊢\neg B\in \mathrm{V}\to B^A\subseteq \left\{f|f:A⟶B\right\}$$
8	3 7	pm2.61i	$$⊢B^A\subseteq \left\{f|f:A⟶B\right\}$$