Theorem mapex

Description: The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of Kunen p. 31. (Contributed by Raph Levien, 4-Dec-2003)

	Ref	Expression
Assertion	mapex	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fssxp	$$⊢f:A⟶B\to f\subseteq A\times B$$
2	1	ss2abi	$$⊢\left\{f|f:A⟶B\right\}\subseteq \left\{f|f\subseteq A\times B\right\}$$
3		df-pw	$$⊢𝒫\left(A\times B\right)=\left\{f|f\subseteq A\times B\right\}$$
4	2 3	sseqtrri	$$⊢\left\{f|f:A⟶B\right\}\subseteq 𝒫\left(A\times B\right)$$
5		xpexg	$$⊢\left(A\in C\wedge B\in D\right)\to A\times B\in \mathrm{V}$$
6	5	pwexd	$$⊢\left(A\in C\wedge B\in D\right)\to 𝒫\left(A\times B\right)\in \mathrm{V}$$
7		ssexg	$$⊢\left(\left\{f|f:A⟶B\right\}\subseteq 𝒫\left(A\times B\right)\wedge 𝒫\left(A\times B\right)\in \mathrm{V}\right)\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$
8	4 6 7	sylancr	$$⊢\left(A\in C\wedge B\in D\right)\to \left\{f|f:A⟶B\right\}\in \mathrm{V}$$