Metamath Proof Explorer

Theorem fvelsetpreimafv

Description: There is an element in a preimage S of function values so that S is the preimage of the function value at this element. (Contributed by AV, 8-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2		preimafvsnel	$⊢ (F Fn A \land x \in A) \to x \in F^{-1} [\{F (x)\}]$
3	2	adantrr	$⊢ (F Fn A \land (x \in A \land S = F^{-1} [\{F (x)\}])) \to x \in F^{-1} [\{F (x)\}]$
4		eleq2	$⊢ S = F^{-1} [\{F (x)\}] \to (x \in S \leftrightarrow x \in F^{-1} [\{F (x)\}])$
5	4	ad2antll	$⊢ (F Fn A \land (x \in A \land S = F^{-1} [\{F (x)\}])) \to (x \in S \leftrightarrow x \in F^{-1} [\{F (x)\}])$
6	3 5	mpbird	$⊢ (F Fn A \land (x \in A \land S = F^{-1} [\{F (x)\}])) \to x \in S$
7		simprr	$⊢ (F Fn A \land (x \in A \land S = F^{-1} [\{F (x)\}])) \to S = F^{-1} [\{F (x)\}]$
8	6 7	jca	$⊢ (F Fn A \land (x \in A \land S = F^{-1} [\{F (x)\}])) \to (x \in S \land S = F^{-1} [\{F (x)\}])$
9	8	ex	$⊢ F Fn A \to ((x \in A \land S = F^{-1} [\{F (x)\}]) \to (x \in S \land S = F^{-1} [\{F (x)\}]))$
10	9	reximdv2	$⊢ F Fn A \to (\exists x \in A S = F^{-1} [\{F (x)\}] \to \exists x \in S S = F^{-1} [\{F (x)\}])$
11	1	elsetpreimafv	$⊢ S \in P \to \exists x \in A S = F^{-1} [\{F (x)\}]$
12	10 11	impel	$⊢ (F Fn A \land S \in P) \to \exists x \in S S = F^{-1} [\{F (x)\}]$