Theorem fnpm

Description: Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Assertion	fnpm	$$⊢{\uparrow }_{𝑝𝑚}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-pm	$$⊢{\uparrow }_{𝑝𝑚}=\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left\{f\in 𝒫\left(y\times x\right)|\mathrm{Fun}f\right\}\right)$$
2		vex	$$⊢y\in \mathrm{V}$$
3		vex	$$⊢x\in \mathrm{V}$$
4	2 3	xpex	$$⊢y\times x\in \mathrm{V}$$
5	4	pwex	$$⊢𝒫\left(y\times x\right)\in \mathrm{V}$$
6	5	rabex	$$⊢\left\{f\in 𝒫\left(y\times x\right)|\mathrm{Fun}f\right\}\in \mathrm{V}$$
7	1 6	fnmpoi	$$⊢{\uparrow }_{𝑝𝑚}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$