# Metamath Proof Explorer

## Theorem elpm2r

Description: Sufficient condition for being a partial function. (Contributed by NM, 31-Dec-2013)

Ref Expression
Assertion elpm2r ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\right)\to {F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)$

### Proof

Step Hyp Ref Expression
1 fdm ${⊢}{F}:{C}⟶{A}\to \mathrm{dom}{F}={C}$
2 1 feq2d ${⊢}{F}:{C}⟶{A}\to \left({F}:\mathrm{dom}{F}⟶{A}↔{F}:{C}⟶{A}\right)$
3 1 sseq1d ${⊢}{F}:{C}⟶{A}\to \left(\mathrm{dom}{F}\subseteq {B}↔{C}\subseteq {B}\right)$
4 2 3 anbi12d ${⊢}{F}:{C}⟶{A}\to \left(\left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)↔\left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\right)$
5 4 adantr ${⊢}\left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\to \left(\left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)↔\left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\right)$
6 5 ibir ${⊢}\left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\to \left({F}:\mathrm{dom}{F}⟶{A}\wedge \mathrm{dom}{F}\subseteq {B}\right)$
7 elpm2g ${⊢}\left({A}\in {V}\wedge {B}\in {W}\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 syl5ibr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\to {F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)\right)$
9 8 imp ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({F}:{C}⟶{A}\wedge {C}\subseteq {B}\right)\right)\to {F}\in \left({A}{↑}_{𝑝𝑚}{B}\right)$