Theorem preimafvelsetpreimafv

Description: The preimage of a function value is an element of the class P of all preimages of function values. (Contributed by AV, 10-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	preimafvelsetpreimafv	$$⊢\left(FFnA\wedge A\in V\wedge X\in A\right)\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in P$$

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		id	$$⊢X\in A\to X\in A$$
3		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
4	3	sneqd	$$⊢x=X\to \left\{F\left(x\right)\right\}=\left\{F\left(X\right)\right\}$$
5	4	imaeq2d	$$⊢x=X\to F^{-1}\left[\left\{F\left(x\right)\right\}\right]=F^{-1}\left[\left\{F\left(X\right)\right\}\right]$$
6	5	eqeq2d	$$⊢x=X\to \left(F^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\leftrightarrow F^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(X\right)\right\}\right]\right)$$
7	6	adantl	$$⊢\left(X\in A\wedge x=X\right)\to \left(F^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\leftrightarrow F^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(X\right)\right\}\right]\right)$$
8		eqidd	$$⊢X\in A\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(X\right)\right\}\right]$$
9	2 7 8	rspcedvd	$$⊢X\in A\to \exists x\in A{F}^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]$$
10	9	3ad2ant3	$$⊢\left(FFnA\wedge A\in V\wedge X\in A\right)\to \exists x\in A{F}^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]$$
11		fnex	$$⊢\left(FFnA\wedge A\in V\right)\to F\in \mathrm{V}$$
12		cnvexg	$$⊢F\in \mathrm{V}\to F^{-1}\in \mathrm{V}$$
13		imaexg	$$⊢F^{-1}\in \mathrm{V}\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in \mathrm{V}$$
14	11 12 13	3syl	$$⊢\left(FFnA\wedge A\in V\right)\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in \mathrm{V}$$
15	14	3adant3	$$⊢\left(FFnA\wedge A\in V\wedge X\in A\right)\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in \mathrm{V}$$
16	1	elsetpreimafvb	$$⊢F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in \mathrm{V}\to \left(F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in P\leftrightarrow \exists x\in A{F}^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
17	15 16	syl	$$⊢\left(FFnA\wedge A\in V\wedge X\in A\right)\to \left(F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in P\leftrightarrow \exists x\in A{F}^{-1}\left[\left\{F\left(X\right)\right\}\right]=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
18	10 17	mpbird	$$⊢\left(FFnA\wedge A\in V\wedge X\in A\right)\to F^{-1}\left[\left\{F\left(X\right)\right\}\right]\in P$$