imasetpreimafvbijlemfv

Description: Lemma for imasetpreimafvbij : the value of the mapping H at a preimage of a value of function F . (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	imasetpreimafvbijlemfv	$⊢ (F Fn A \land Y \in P \land X \in Y) \to H (Y) = F (X)$

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		fnfun	$⊢ F Fn A \to Fun F$
4	3	anim1i	$⊢ (F Fn A \land Y \in P) \to (Fun F \land Y \in P)$
5	4	3adant3	$⊢ (F Fn A \land Y \in P \land X \in Y) \to (Fun F \land Y \in P)$
6	1 2	fundcmpsurinjlem3	$⊢ (Fun F \land Y \in P) \to H (Y) = ⋃ F [Y]$
7	5 6	syl	$⊢ (F Fn A \land Y \in P \land X \in Y) \to H (Y) = ⋃ F [Y]$
8	3	3ad2ant1	$⊢ (F Fn A \land Y \in P \land X \in Y) \to Fun F$
9		funiunfv	$⊢ Fun F \to ⋃_{y \in Y} F (y) = ⋃ F [Y]$
10	8 9	syl	$⊢ (F Fn A \land Y \in P \land X \in Y) \to ⋃_{y \in Y} F (y) = ⋃ F [Y]$
11		simp3	$⊢ (F Fn A \land Y \in P \land X \in Y) \to X \in Y$
12		simpl1	$⊢ ((F Fn A \land Y \in P \land X \in Y) \land y \in Y) \to F Fn A$
13		simpl2	$⊢ ((F Fn A \land Y \in P \land X \in Y) \land y \in Y) \to Y \in P$
14		simpr	$⊢ ((F Fn A \land Y \in P \land X \in Y) \land y \in Y) \to y \in Y$
15		simpl3	$⊢ ((F Fn A \land Y \in P \land X \in Y) \land y \in Y) \to X \in Y$
16	1	elsetpreimafveqfv	$⊢ (F Fn A \land (Y \in P \land y \in Y \land X \in Y)) \to F (y) = F (X)$
17	12 13 14 15 16	syl13anc	$⊢ ((F Fn A \land Y \in P \land X \in Y) \land y \in Y) \to F (y) = F (X)$
18	17	ralrimiva	$⊢ (F Fn A \land Y \in P \land X \in Y) \to \forall y \in Y F (y) = F (X)$
19		fveq2	$⊢ y = X \to F (y) = F (X)$
20	19	iuneqconst	$⊢ (X \in Y \land \forall y \in Y F (y) = F (X)) \to ⋃_{y \in Y} F (y) = F (X)$
21	11 18 20	syl2anc	$⊢ (F Fn A \land Y \in P \land X \in Y) \to ⋃_{y \in Y} F (y) = F (X)$
22	7 10 21	3eqtr2d	$⊢ (F Fn A \land Y \in P \land X \in Y) \to H (Y) = F (X)$

Metamath Proof Explorer

Theorem imasetpreimafvbijlemfv

Proof