Metamath Proof Explorer

Theorem imasetpreimafvbijlemfv1

Description: Lemma for imasetpreimafvbij : for a preimage of a value of function F there is an element of the preimage so that the value of the mapping H at this preimage is the function value at this element. (Contributed by AV, 5-Mar-2024)

		Ref	Expression
	Hypotheses	fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
		fundcmpsurinj.h	$⊢ H = (p \in P ⟼ ⋃ F [p])$
	Assertion	imasetpreimafvbijlemfv1	$⊢ (F Fn A \land X \in P) \to \exists y \in X H (X) = F (y)$

Proof

Step	Hyp	Ref	Expression
1		fundcmpsurinj.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2		fundcmpsurinj.h	$⊢ H = (p \in P ⟼ ⋃ F [p])$
3	1	0nelsetpreimafv	$⊢ F Fn A \to \emptyset \notin P$
4		elnelne2	$⊢ (X \in P \land \emptyset \notin P) \to X \neq \emptyset$
5	4	expcom	$⊢ \emptyset \notin P \to (X \in P \to X \neq \emptyset)$
6	3 5	syl	$⊢ F Fn A \to (X \in P \to X \neq \emptyset)$
7	6	imp	$⊢ (F Fn A \land X \in P) \to X \neq \emptyset$
8		simpr	$⊢ ((F Fn A \land X \in P) \land y \in X) \to y \in X$
9	1 2	imasetpreimafvbijlemfv	$⊢ (F Fn A \land X \in P \land y \in X) \to H (X) = F (y)$
10	9	3expa	$⊢ ((F Fn A \land X \in P) \land y \in X) \to H (X) = F (y)$
11	8 10	jca	$⊢ ((F Fn A \land X \in P) \land y \in X) \to (y \in X \land H (X) = F (y))$
12	11	ex	$⊢ (F Fn A \land X \in P) \to (y \in X \to (y \in X \land H (X) = F (y)))$
13	12	eximdv	$⊢ (F Fn A \land X \in P) \to (\exists y y \in X \to \exists y (y \in X \land H (X) = F (y)))$
14		n0	$⊢ X \neq \emptyset \leftrightarrow \exists y y \in X$
15		df-rex	$⊢ \exists y \in X H (X) = F (y) \leftrightarrow \exists y (y \in X \land H (X) = F (y))$
16	13 14 15	3imtr4g	$⊢ (F Fn A \land X \in P) \to (X \neq \emptyset \to \exists y \in X H (X) = F (y))$
17	7 16	mpd	$⊢ (F Fn A \land X \in P) \to \exists y \in X H (X) = F (y)$