Theorem preimane

Description: Different elements have different preimages. (Contributed by Thierry Arnoux, 7-May-2023)

	Ref	Expression
Hypotheses	preimane.f	$$⊢\phi \to \mathrm{Fun}F$$
	preimane.x	$$⊢\phi \to X\ne Y$$
	preimane.y	$$⊢\phi \to X\in \mathrm{ran}F$$
	preimane.1	$$⊢\phi \to Y\in \mathrm{ran}F$$
Assertion	preimane	$$⊢\phi \to F^{-1}\left[\left\{X\right\}\right]\ne F^{-1}\left[\left\{Y\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		preimane.f	$$⊢\phi \to \mathrm{Fun}F$$
2		preimane.x	$$⊢\phi \to X\ne Y$$
3		preimane.y	$$⊢\phi \to X\in \mathrm{ran}F$$
4		preimane.1	$$⊢\phi \to Y\in \mathrm{ran}F$$
5		sneqrg	$$⊢X\in \mathrm{ran}F\to \left(\left\{X\right\}=\left\{Y\right\}\to X=Y\right)$$
6	3 5	syl	$$⊢\phi \to \left(\left\{X\right\}=\left\{Y\right\}\to X=Y\right)$$
7	6	necon3d	$$⊢\phi \to \left(X\ne Y\to \left\{X\right\}\ne \left\{Y\right\}\right)$$
8	2 7	mpd	$$⊢\phi \to \left\{X\right\}\ne \left\{Y\right\}$$
9		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[\left\{X\right\}\right]\right]=\left\{X\right\}\cap \mathrm{ran}F$$
10	1 9	syl	$$⊢\phi \to F\left[F^{-1}\left[\left\{X\right\}\right]\right]=\left\{X\right\}\cap \mathrm{ran}F$$
11	3	snssd	$$⊢\phi \to \left\{X\right\}\subseteq \mathrm{ran}F$$
12		dfss2	$$⊢\left\{X\right\}\subseteq \mathrm{ran}F\leftrightarrow \left\{X\right\}\cap \mathrm{ran}F=\left\{X\right\}$$
13	11 12	sylib	$$⊢\phi \to \left\{X\right\}\cap \mathrm{ran}F=\left\{X\right\}$$
14	10 13	eqtrd	$$⊢\phi \to F\left[F^{-1}\left[\left\{X\right\}\right]\right]=\left\{X\right\}$$
15		funimacnv	$$⊢\mathrm{Fun}F\to F\left[F^{-1}\left[\left\{Y\right\}\right]\right]=\left\{Y\right\}\cap \mathrm{ran}F$$
16	1 15	syl	$$⊢\phi \to F\left[F^{-1}\left[\left\{Y\right\}\right]\right]=\left\{Y\right\}\cap \mathrm{ran}F$$
17	4	snssd	$$⊢\phi \to \left\{Y\right\}\subseteq \mathrm{ran}F$$
18		dfss2	$$⊢\left\{Y\right\}\subseteq \mathrm{ran}F\leftrightarrow \left\{Y\right\}\cap \mathrm{ran}F=\left\{Y\right\}$$
19	17 18	sylib	$$⊢\phi \to \left\{Y\right\}\cap \mathrm{ran}F=\left\{Y\right\}$$
20	16 19	eqtrd	$$⊢\phi \to F\left[F^{-1}\left[\left\{Y\right\}\right]\right]=\left\{Y\right\}$$
21	8 14 20	3netr4d	$$⊢\phi \to F\left[F^{-1}\left[\left\{X\right\}\right]\right]\ne F\left[F^{-1}\left[\left\{Y\right\}\right]\right]$$
22		imaeq2	$$⊢F^{-1}\left[\left\{X\right\}\right]=F^{-1}\left[\left\{Y\right\}\right]\to F\left[F^{-1}\left[\left\{X\right\}\right]\right]=F\left[F^{-1}\left[\left\{Y\right\}\right]\right]$$
23	22	necon3i	$$⊢F\left[F^{-1}\left[\left\{X\right\}\right]\right]\ne F\left[F^{-1}\left[\left\{Y\right\}\right]\right]\to F^{-1}\left[\left\{X\right\}\right]\ne F^{-1}\left[\left\{Y\right\}\right]$$
24	21 23	syl	$$⊢\phi \to F^{-1}\left[\left\{X\right\}\right]\ne F^{-1}\left[\left\{Y\right\}\right]$$