Theorem elpmrn

Description: The range of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

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	1	simpld	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to F:\mathrm{dom}F⟶A$$
3	2	frnd	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \mathrm{ran}F\subseteq A$$