Theorem pmfun

Description: A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	pmfun	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \mathrm{Fun}F$$

Proof

Step	Hyp	Ref	Expression
1		elpmi	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \left(F:\mathrm{dom}F⟶A\wedge \mathrm{dom}F\subseteq B\right)$$
2		ffun	$$⊢F:\mathrm{dom}F⟶A\to \mathrm{Fun}F$$
3	2	adantr	$$⊢\left(F:\mathrm{dom}F⟶A\wedge \mathrm{dom}F\subseteq B\right)\to \mathrm{Fun}F$$
4	1 3	syl	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \mathrm{Fun}F$$