fvelima2

Description: Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Assertion	fvelima2	$⊢ (F Fn A \land B \in F [C]) \to \exists x \in (A \cap C) F (x) = B$

Step	Hyp	Ref	Expression
1		elimag	$⊢ B \in F [C] \to (B \in F [C] \leftrightarrow \exists x \in C x F B)$
2	1	ibi	$⊢ B \in F [C] \to \exists x \in C x F B$
3		df-rex	$⊢ \exists x \in C x F B \leftrightarrow \exists x (x \in C \land x F B)$
4	2 3	sylib	$⊢ B \in F [C] \to \exists x (x \in C \land x F B)$
5		fnbr	$⊢ (F Fn A \land x F B) \to x \in A$
6	5	adantrl	$⊢ (F Fn A \land (x \in C \land x F B)) \to x \in A$
7		simprl	$⊢ (F Fn A \land (x \in C \land x F B)) \to x \in C$
8	6 7	elind	$⊢ (F Fn A \land (x \in C \land x F B)) \to x \in (A \cap C)$
9		fnfun	$⊢ F Fn A \to Fun F$
10		funbrfv	$⊢ Fun F \to (x F B \to F (x) = B)$
11	10	imp	$⊢ (Fun F \land x F B) \to F (x) = B$
12	9 11	sylan	$⊢ (F Fn A \land x F B) \to F (x) = B$
13	12	adantrl	$⊢ (F Fn A \land (x \in C \land x F B)) \to F (x) = B$
14	8 13	jca	$⊢ (F Fn A \land (x \in C \land x F B)) \to (x \in (A \cap C) \land F (x) = B)$
15	14	ex	$⊢ F Fn A \to ((x \in C \land x F B) \to (x \in (A \cap C) \land F (x) = B))$
16	15	eximdv	$⊢ F Fn A \to (\exists x (x \in C \land x F B) \to \exists x (x \in (A \cap C) \land F (x) = B))$
17	16	imp	$⊢ (F Fn A \land \exists x (x \in C \land x F B)) \to \exists x (x \in (A \cap C) \land F (x) = B)$
18		df-rex	$⊢ \exists x \in (A \cap C) F (x) = B \leftrightarrow \exists x (x \in (A \cap C) \land F (x) = B)$
19	17 18	sylibr	$⊢ (F Fn A \land \exists x (x \in C \land x F B)) \to \exists x \in (A \cap C) F (x) = B$
20	4 19	sylan2	$⊢ (F Fn A \land B \in F [C]) \to \exists x \in (A \cap C) F (x) = B$

Metamath Proof Explorer