Metamath Proof Explorer

Theorem uniimafveqt

Description: The union of the image of a subset S of the domain of a function with elements having the same function value is the function value at one of the elements of S . (Contributed by AV, 5-Mar-2024)

		Ref	Expression
	Assertion	uniimafveqt	$⊢ (F : A ⟶ B \land S \subseteq A \land X \in S) \to (\forall x \in S F (x) = F (X) \to ⋃ F [S] = F (X))$

Proof

Step	Hyp	Ref	Expression
1		ffun	$⊢ F : A ⟶ B \to Fun F$
2	1	3ad2ant1	$⊢ (F : A ⟶ B \land S \subseteq A \land X \in S) \to Fun F$
3	2	adantr	$⊢ ((F : A ⟶ B \land S \subseteq A \land X \in S) \land \forall x \in S F (x) = F (X)) \to Fun F$
4		funiunfv	$⊢ Fun F \to ⋃_{y \in S} F (y) = ⋃ F [S]$
5	3 4	syl	$⊢ ((F : A ⟶ B \land S \subseteq A \land X \in S) \land \forall x \in S F (x) = F (X)) \to ⋃_{y \in S} F (y) = ⋃ F [S]$
6		simp3	$⊢ (F : A ⟶ B \land S \subseteq A \land X \in S) \to X \in S$
7		fveqeq2	$⊢ x = y \to (F (x) = F (X) \leftrightarrow F (y) = F (X))$
8	7	cbvralvw	$⊢ \forall x \in S F (x) = F (X) \leftrightarrow \forall y \in S F (y) = F (X)$
9	8	biimpi	$⊢ \forall x \in S F (x) = F (X) \to \forall y \in S F (y) = F (X)$
10		fveq2	$⊢ y = X \to F (y) = F (X)$
11	10	iuneqconst	$⊢ (X \in S \land \forall y \in S F (y) = F (X)) \to ⋃_{y \in S} F (y) = F (X)$
12	6 9 11	syl2an	$⊢ ((F : A ⟶ B \land S \subseteq A \land X \in S) \land \forall x \in S F (x) = F (X)) \to ⋃_{y \in S} F (y) = F (X)$
13	5 12	eqtr3d	$⊢ ((F : A ⟶ B \land S \subseteq A \land X \in S) \land \forall x \in S F (x) = F (X)) \to ⋃ F [S] = F (X)$
14	13	ex	$⊢ (F : A ⟶ B \land S \subseteq A \land X \in S) \to (\forall x \in S F (x) = F (X) \to ⋃ F [S] = F (X))$