| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fnpm | Structured version Visualization version GIF version | ||
| Description: Partial function exponentiation has a universal domain. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| Ref | Expression |
|---|---|
| fnpm | ⊢ ↑pm Fn (V × V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-pm 8767 | . 2 ⊢ ↑pm = (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓}) | |
| 2 | vex 3434 | . . . . 5 ⊢ 𝑦 ∈ V | |
| 3 | vex 3434 | . . . . 5 ⊢ 𝑥 ∈ V | |
| 4 | 2, 3 | xpex 7698 | . . . 4 ⊢ (𝑦 × 𝑥) ∈ V |
| 5 | 4 | pwex 5315 | . . 3 ⊢ 𝒫 (𝑦 × 𝑥) ∈ V |
| 6 | 5 | rabex 5274 | . 2 ⊢ {𝑓 ∈ 𝒫 (𝑦 × 𝑥) ∣ Fun 𝑓} ∈ V |
| 7 | 1, 6 | fnmpoi 8014 | 1 ⊢ ↑pm Fn (V × V) |
| Colors of variables: wff setvar class |
| Syntax hints: {crab 3390 Vcvv 3430 𝒫 cpw 4542 × cxp 5620 Fun wfun 6484 Fn wfn 6485 ↑pm cpm 8765 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-fv 6498 df-oprab 7362 df-mpo 7363 df-1st 7933 df-2nd 7934 df-pm 8767 |
| This theorem is referenced by: elpmi 8784 pmresg 8809 pmsspw 8816 |
| Copyright terms: Public domain | W3C validator |