Theorem mptelpm

Description: A function in maps-to notation is a partial map . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	mptelpm.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	mptelpm.a	$$⊢\phi \to A\subseteq D$$
	mptelpm.c	$$⊢\phi \to C\in V$$
	mptelpm.d	$$⊢\phi \to D\in W$$
Assertion	mptelpm	$$⊢\phi \to \left(x\in A⟼B\right)\in \left(C{\uparrow }_{𝑝𝑚}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptelpm.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
2		mptelpm.a	$$⊢\phi \to A\subseteq D$$
3		mptelpm.c	$$⊢\phi \to C\in V$$
4		mptelpm.d	$$⊢\phi \to D\in W$$
5	1	fmpttd	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
6		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
7	6 1	dmmptd	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼B\right)=A$$
8	7	eqcomd	$$⊢\phi \to A=\mathrm{dom}\left(x\in A⟼B\right)$$
9	8	feq2d	$$⊢\phi \to \left(\left(x\in A⟼B\right):A⟶C\leftrightarrow \left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶C\right)$$
10	5 9	mpbid	$$⊢\phi \to \left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶C$$
11	7 2	eqsstrd	$$⊢\phi \to \mathrm{dom}\left(x\in A⟼B\right)\subseteq D$$
12	10 11	jca	$$⊢\phi \to \left(\left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶C\wedge \mathrm{dom}\left(x\in A⟼B\right)\subseteq D\right)$$
13		elpm2g	$$⊢\left(C\in V\wedge D\in W\right)\to \left(\left(x\in A⟼B\right)\in \left(C{\uparrow }_{𝑝𝑚}D\right)\leftrightarrow \left(\left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶C\wedge \mathrm{dom}\left(x\in A⟼B\right)\subseteq D\right)\right)$$
14	3 4 13	syl2anc	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in \left(C{\uparrow }_{𝑝𝑚}D\right)\leftrightarrow \left(\left(x\in A⟼B\right):\mathrm{dom}\left(x\in A⟼B\right)⟶C\wedge \mathrm{dom}\left(x\in A⟼B\right)\subseteq D\right)\right)$$
15	12 14	mpbird	$$⊢\phi \to \left(x\in A⟼B\right)\in \left(C{\uparrow }_{𝑝𝑚}D\right)$$