Theorem fpmd

Description: A total function is a partial function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	fpmd.a	$$⊢\phi \to A\in V$$
	fpmd.b	$$⊢\phi \to B\in W$$
	fpmd.c	$$⊢\phi \to C\subseteq A$$
	fpmd.f	$$⊢\phi \to F:C⟶B$$
Assertion	fpmd	$$⊢\phi \to F\in \left(B{\uparrow }_{𝑝𝑚}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fpmd.a	$$⊢\phi \to A\in V$$
2		fpmd.b	$$⊢\phi \to B\in W$$
3		fpmd.c	$$⊢\phi \to C\subseteq A$$
4		fpmd.f	$$⊢\phi \to F:C⟶B$$
5		elpm2r	$$⊢\left(\left(B\in W\wedge A\in V\right)\wedge \left(F:C⟶B\wedge C\subseteq A\right)\right)\to F\in \left(B{\uparrow }_{𝑝𝑚}A\right)$$
6	2 1 4 3 5	syl22anc	$$⊢\phi \to F\in \left(B{\uparrow }_{𝑝𝑚}A\right)$$