Metamath Proof Explorer

Theorem elsetpreimafveq

Description: If two preimages of function values contain elements with identical function values, then both preimages are equal. (Contributed by AV, 8-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2		eqeq2	$⊢ F (X) = F (Y) \to (F (x) = F (X) \leftrightarrow F (x) = F (Y))$
3	2	rabbidv	$⊢ F (X) = F (Y) \to \{x \in A \| F (x) = F (X)\} = \{x \in A \| F (x) = F (Y)\}$
4	3	adantl	$⊢ ((F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \land F (X) = F (Y)) \to \{x \in A \| F (x) = F (X)\} = \{x \in A \| F (x) = F (Y)\}$
5		id	$⊢ F Fn A \to F Fn A$
6		simpl	$⊢ (S \in P \land R \in P) \to S \in P$
7		simpl	$⊢ (X \in S \land Y \in R) \to X \in S$
8	5 6 7	3anim123i	$⊢ (F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \to (F Fn A \land S \in P \land X \in S)$
9	8	adantr	$⊢ ((F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \land F (X) = F (Y)) \to (F Fn A \land S \in P \land X \in S)$
10	1	elsetpreimafvrab	$⊢ (F Fn A \land S \in P \land X \in S) \to S = \{x \in A \| F (x) = F (X)\}$
11	9 10	syl	$⊢ ((F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \land F (X) = F (Y)) \to S = \{x \in A \| F (x) = F (X)\}$
12		simpr	$⊢ (S \in P \land R \in P) \to R \in P$
13		simpr	$⊢ (X \in S \land Y \in R) \to Y \in R$
14	5 12 13	3anim123i	$⊢ (F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \to (F Fn A \land R \in P \land Y \in R)$
15	14	adantr	$⊢ ((F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \land F (X) = F (Y)) \to (F Fn A \land R \in P \land Y \in R)$
16	1	elsetpreimafvrab	$⊢ (F Fn A \land R \in P \land Y \in R) \to R = \{x \in A \| F (x) = F (Y)\}$
17	15 16	syl	$⊢ ((F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \land F (X) = F (Y)) \to R = \{x \in A \| F (x) = F (Y)\}$
18	4 11 17	3eqtr4d	$⊢ ((F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \land F (X) = F (Y)) \to S = R$
19	18	ex	$⊢ (F Fn A \land (S \in P \land R \in P) \land (X \in S \land Y \in R)) \to (F (X) = F (Y) \to S = R)$