imaelsetpreimafv

Description: The image of an element of the preimage of a function value is the singleton consisting of the function value at one of its elements. (Contributed by AV, 5-Mar-2024)

		Ref	Expression
	Hypothesis	setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
	Assertion	imaelsetpreimafv	$⊢ (F Fn A \land S \in P \land X \in S) \to F [S] = \{F (X)\}$

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2	1	fvelsetpreimafv	$⊢ (F Fn A \land S \in P) \to \exists x \in S S = F^{-1} [\{F (x)\}]$
3		fveq2	$⊢ y = x \to F (y) = F (x)$
4	3	sneqd	$⊢ y = x \to \{F (y)\} = \{F (x)\}$
5	4	imaeq2d	$⊢ y = x \to F^{-1} [\{F (y)\}] = F^{-1} [\{F (x)\}]$
6	5	eqeq2d	$⊢ y = x \to (S = F^{-1} [\{F (y)\}] \leftrightarrow S = F^{-1} [\{F (x)\}])$
7	6	cbvrexvw	$⊢ \exists y \in S S = F^{-1} [\{F (y)\}] \leftrightarrow \exists x \in S S = F^{-1} [\{F (x)\}]$
8	2 7	sylibr	$⊢ (F Fn A \land S \in P) \to \exists y \in S S = F^{-1} [\{F (y)\}]$
9	8	3adant3	$⊢ (F Fn A \land S \in P \land X \in S) \to \exists y \in S S = F^{-1} [\{F (y)\}]$
10		imaeq2	$⊢ S = F^{-1} [\{F (y)\}] \to F [S] = F [F^{-1} [\{F (y)\}]]$
11	10	3ad2ant3	$⊢ ((F Fn A \land S \in P \land X \in S) \land y \in S \land S = F^{-1} [\{F (y)\}]) \to F [S] = F [F^{-1} [\{F (y)\}]]$
12		fnfun	$⊢ F Fn A \to Fun F$
13		funimacnv	$⊢ Fun F \to F [F^{-1} [\{F (y)\}]] = \{F (y)\} \cap ran F$
14	12 13	syl	$⊢ F Fn A \to F [F^{-1} [\{F (y)\}]] = \{F (y)\} \cap ran F$
15	14	3ad2ant1	$⊢ (F Fn A \land S \in P \land X \in S) \to F [F^{-1} [\{F (y)\}]] = \{F (y)\} \cap ran F$
16	15	3ad2ant1	$⊢ ((F Fn A \land S \in P \land X \in S) \land y \in S \land S = F^{-1} [\{F (y)\}]) \to F [F^{-1} [\{F (y)\}]] = \{F (y)\} \cap ran F$
17	1	elsetpreimafvbi	$⊢ (F Fn A \land S \in P \land X \in S) \to (y \in S \leftrightarrow (y \in A \land F (y) = F (X)))$
18		fnfvelrn	$⊢ (F Fn A \land y \in A) \to F (y) \in ran F$
19	18	snssd	$⊢ (F Fn A \land y \in A) \to \{F (y)\} \subseteq ran F$
20		dfss2	$⊢ \{F (y)\} \subseteq ran F \leftrightarrow \{F (y)\} \cap ran F = \{F (y)\}$
21	19 20	sylib	$⊢ (F Fn A \land y \in A) \to \{F (y)\} \cap ran F = \{F (y)\}$
22	21	3adant3	$⊢ (F Fn A \land y \in A \land F (y) = F (X)) \to \{F (y)\} \cap ran F = \{F (y)\}$
23		simp3	$⊢ (F Fn A \land y \in A \land F (y) = F (X)) \to F (y) = F (X)$
24	23	sneqd	$⊢ (F Fn A \land y \in A \land F (y) = F (X)) \to \{F (y)\} = \{F (X)\}$
25	22 24	eqtrd	$⊢ (F Fn A \land y \in A \land F (y) = F (X)) \to \{F (y)\} \cap ran F = \{F (X)\}$
26	25	3expib	$⊢ F Fn A \to ((y \in A \land F (y) = F (X)) \to \{F (y)\} \cap ran F = \{F (X)\})$
27	26	3ad2ant1	$⊢ (F Fn A \land S \in P \land X \in S) \to ((y \in A \land F (y) = F (X)) \to \{F (y)\} \cap ran F = \{F (X)\})$
28	17 27	sylbid	$⊢ (F Fn A \land S \in P \land X \in S) \to (y \in S \to \{F (y)\} \cap ran F = \{F (X)\})$
29	28	imp	$⊢ ((F Fn A \land S \in P \land X \in S) \land y \in S) \to \{F (y)\} \cap ran F = \{F (X)\}$
30	29	3adant3	$⊢ ((F Fn A \land S \in P \land X \in S) \land y \in S \land S = F^{-1} [\{F (y)\}]) \to \{F (y)\} \cap ran F = \{F (X)\}$
31	11 16 30	3eqtrd	$⊢ ((F Fn A \land S \in P \land X \in S) \land y \in S \land S = F^{-1} [\{F (y)\}]) \to F [S] = \{F (X)\}$
32	31	rexlimdv3a	$⊢ (F Fn A \land S \in P \land X \in S) \to (\exists y \in S S = F^{-1} [\{F (y)\}] \to F [S] = \{F (X)\})$
33	9 32	mpd	$⊢ (F Fn A \land S \in P \land X \in S) \to F [S] = \{F (X)\}$

Metamath Proof Explorer

Theorem imaelsetpreimafv

Proof