# Metamath Proof Explorer

## Theorem elpmi

Description: A partial function is a function. (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Assertion elpmi ${⊢}{F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)\to \left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)$

### Proof

Step Hyp Ref Expression
1 n0i ${⊢}{F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)\to ¬{A}{↑}_{𝑝𝑚}{B}=\varnothing$
2 fnpm ${⊢}{↑}_{𝑝𝑚}Fn\left(\mathrm{V}×\mathrm{V}\right)$
3 fndm ${⊢}{↑}_{𝑝𝑚}Fn\left(\mathrm{V}×\mathrm{V}\right)\to \mathrm{dom}{↑}_{𝑝𝑚}=\mathrm{V}×\mathrm{V}$
4 2 3 ax-mp ${⊢}\mathrm{dom}{↑}_{𝑝𝑚}=\mathrm{V}×\mathrm{V}$
5 4 ndmov ${⊢}¬\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to {A}{↑}_{𝑝𝑚}{B}=\varnothing$
6 1 5 nsyl2 ${⊢}{F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
7 elpm2g ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left({F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)↔\left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)\right)$
8 6 7 syl ${⊢}{F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)\to \left({F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)↔\left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)\right)$
9 8 ibi ${⊢}{F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)\to \left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)$