Metamath Proof Explorer

Theorem elsetpreimafvbi

Description: An element of the preimage of a function value is an element of the domain of the function with the same value as another element of the preimage. (Contributed by AV, 9-Mar-2024)

		Ref	Expression
	Hypothesis	setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2		fniniseg	$⊢ F Fn A \to (X \in F^{-1} [\{F (x)\}] \leftrightarrow (X \in A \land F (X) = F (x)))$
3		fniniseg	$⊢ F Fn A \to (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (x)))$
4		eqeq2	$⊢ F (x) = F (X) \to (F (Y) = F (x) \leftrightarrow F (Y) = F (X))$
5	4	anbi2d	$⊢ F (x) = F (X) \to ((Y \in A \land F (Y) = F (x)) \leftrightarrow (Y \in A \land F (Y) = F (X)))$
6	5	eqcoms	$⊢ F (X) = F (x) \to ((Y \in A \land F (Y) = F (x)) \leftrightarrow (Y \in A \land F (Y) = F (X)))$
7	3 6	sylan9bb	$⊢ (F Fn A \land F (X) = F (x)) \to (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (X)))$
8	7	ex	$⊢ F Fn A \to (F (X) = F (x) \to (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (X))))$
9	8	adantld	$⊢ F Fn A \to ((X \in A \land F (X) = F (x)) \to (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (X))))$
10	2 9	sylbid	$⊢ F Fn A \to (X \in F^{-1} [\{F (x)\}] \to (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (X))))$
11		eleq2	$⊢ S = F^{-1} [\{F (x)\}] \to (X \in S \leftrightarrow X \in F^{-1} [\{F (x)\}])$
12		eleq2	$⊢ S = F^{-1} [\{F (x)\}] \to (Y \in S \leftrightarrow Y \in F^{-1} [\{F (x)\}])$
13	12	bibi1d	$⊢ S = F^{-1} [\{F (x)\}] \to ((Y \in S \leftrightarrow (Y \in A \land F (Y) = F (X))) \leftrightarrow (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (X))))$
14	11 13	imbi12d	$⊢ S = F^{-1} [\{F (x)\}] \to ((X \in S \to (Y \in S \leftrightarrow (Y \in A \land F (Y) = F (X)))) \leftrightarrow (X \in F^{-1} [\{F (x)\}] \to (Y \in F^{-1} [\{F (x)\}] \leftrightarrow (Y \in A \land F (Y) = F (X)))))$
15	10 14	syl5ibr	$⊢ S = F^{-1} [\{F (x)\}] \to (F Fn A \to (X \in S \to (Y \in S \leftrightarrow (Y \in A \land F (Y) = F (X)))))$
16	15	rexlimivw	$⊢ \exists x \in A S = F^{-1} [\{F (x)\}] \to (F Fn A \to (X \in S \to (Y \in S \leftrightarrow (Y \in A \land F (Y) = F (X)))))$
17	1	elsetpreimafv	$⊢ S \in P \to \exists x \in A S = F^{-1} [\{F (x)\}]$
18	16 17	syl11	$⊢ F Fn A \to (S \in P \to (X \in S \to (Y \in S \leftrightarrow (Y \in A \land F (Y) = F (X)))))$
19	18	3imp	$⊢ (F Fn A \land S \in P \land X \in S) \to (Y \in S \leftrightarrow (Y \in A \land F (Y) = F (X)))$