Description: Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | fnpm | |- ^pm Fn ( _V X. _V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pm | |- ^pm = ( x e. _V , y e. _V |-> { f e. ~P ( y X. x ) | Fun f } ) |
|
2 | vex | |- y e. _V |
|
3 | vex | |- x e. _V |
|
4 | 2 3 | xpex | |- ( y X. x ) e. _V |
5 | 4 | pwex | |- ~P ( y X. x ) e. _V |
6 | 5 | rabex | |- { f e. ~P ( y X. x ) | Fun f } e. _V |
7 | 1 6 | fnmpoi | |- ^pm Fn ( _V X. _V ) |