Theorem preimafvsspwdm

Description: The class P of all preimages of function values is a subset of the power set of the domain of the function. (Contributed by AV, 5-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	$$⊢P=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
Assertion	preimafvsspwdm	$$⊢FFnA\to P\subseteq 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$$⊢P=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
2	1	elsetpreimafvssdm	$$⊢\left(FFnA\wedge s\in P\right)\to s\subseteq A$$
3	2	ralrimiva	$$⊢FFnA\to \forall s\in Ps\subseteq A$$
4		pwssb	$$⊢P\subseteq 𝒫A\leftrightarrow \forall s\in Ps\subseteq A$$
5	3 4	sylibr	$$⊢FFnA\to P\subseteq 𝒫A$$