Metamath Proof Explorer


Theorem fnpm

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

Ref Expression
Assertion fnpm 𝑝𝑚FnV×V

Proof

Step Hyp Ref Expression
1 df-pm 𝑝𝑚=xV,yVf𝒫y×x|Funf
2 vex yV
3 vex xV
4 2 3 xpex y×xV
5 4 pwex 𝒫y×xV
6 5 rabex f𝒫y×x|FunfV
7 1 6 fnmpoi 𝑝𝑚FnV×V