This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnpm

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

Ref Expression
Assertion fnpm ⊢ ↑ 𝑝𝑚 Fn V × V

Proof

Step Hyp Ref Expression
1 df-pm ⊢ ↑ 𝑝𝑚 = x ∈ V , y ∈ V ⟼ f ∈ 𝒫 y × x | Fun ⁡ f
2 vex ⊢ y ∈ V
3 vex ⊢ x ∈ V
4 2 3 xpex ⊢ y × x ∈ V
5 4 pwex ⊢ 𝒫 y × x ∈ V
6 5 rabex ⊢ f ∈ 𝒫 y × x | Fun ⁡ f ∈ V
7 1 6 fnmpoi ⊢ ↑ 𝑝𝑚 Fn V × V