Theorem elsetpreimafvssdm

Description: An element of the class P of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-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	elsetpreimafvssdm	$$⊢\left(FFnA\wedge S\in P\right)\to S\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	elsetpreimafv	$$⊢S\in P\to \exists x\in AS=F^{-1}\left[\left\{F\left(x\right)\right\}\right]$$
3		cnvimass	$$⊢F^{-1}\left[\left\{F\left(x\right)\right\}\right]\subseteq \mathrm{dom}F$$
4		fndm	$$⊢FFnA\to \mathrm{dom}F=A$$
5	3 4	sseqtrid	$$⊢FFnA\to F^{-1}\left[\left\{F\left(x\right)\right\}\right]\subseteq A$$
6	5	adantr	$$⊢\left(FFnA\wedge x\in A\right)\to F^{-1}\left[\left\{F\left(x\right)\right\}\right]\subseteq A$$
7		sseq1	$$⊢S=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\to \left(S\subseteq A\leftrightarrow F^{-1}\left[\left\{F\left(x\right)\right\}\right]\subseteq A\right)$$
8	6 7	syl5ibrcom	$$⊢\left(FFnA\wedge x\in A\right)\to \left(S=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\to S\subseteq A\right)$$
9	8	expcom	$$⊢x\in A\to \left(FFnA\to \left(S=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\to S\subseteq A\right)\right)$$
10	9	com23	$$⊢x\in A\to \left(S=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\to \left(FFnA\to S\subseteq A\right)\right)$$
11	10	rexlimiv	$$⊢\exists x\in AS=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\to \left(FFnA\to S\subseteq A\right)$$
12	2 11	syl	$$⊢S\in P\to \left(FFnA\to S\subseteq A\right)$$
13	12	impcom	$$⊢\left(FFnA\wedge S\in P\right)\to S\subseteq A$$