uniimaelsetpreimafv

Description: The union of the image of an element of the preimage of a function value is an element of the range of the function. (Contributed by AV, 5-Mar-2024) (Revised by AV, 22-Mar-2024)

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

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$⊢ P = \{z \| \exists x \in A z = F^{-1} [\{F (x)\}]\}$
2	1	0nelsetpreimafv	$⊢ F Fn A \to \emptyset \notin P$
3		elnelne2	$⊢ (S \in P \land \emptyset \notin P) \to S \neq \emptyset$
4		n0	$⊢ S \neq \emptyset \leftrightarrow \exists y y \in S$
5	3 4	sylib	$⊢ (S \in P \land \emptyset \notin P) \to \exists y y \in S$
6	5	expcom	$⊢ \emptyset \notin P \to (S \in P \to \exists y y \in S)$
7	2 6	syl	$⊢ F Fn A \to (S \in P \to \exists y y \in S)$
8	7	imp	$⊢ (F Fn A \land S \in P) \to \exists y y \in S$
9	1	imaelsetpreimafv	$⊢ (F Fn A \land S \in P \land y \in S) \to F [S] = \{F (y)\}$
10	9	3expa	$⊢ ((F Fn A \land S \in P) \land y \in S) \to F [S] = \{F (y)\}$
11	10	unieqd	$⊢ ((F Fn A \land S \in P) \land y \in S) \to ⋃ F [S] = ⋃ \{F (y)\}$
12		fvex	$⊢ F (y) \in V$
13	12	unisn	$⊢ ⋃ \{F (y)\} = F (y)$
14	11 13	eqtrdi	$⊢ ((F Fn A \land S \in P) \land y \in S) \to ⋃ F [S] = F (y)$
15		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
16	15	biimpi	$⊢ F Fn A \to F : A ⟶ ran F$
17	16	ad2antrr	$⊢ ((F Fn A \land S \in P) \land y \in S) \to F : A ⟶ ran F$
18	1	elsetpreimafvssdm	$⊢ (F Fn A \land S \in P) \to S \subseteq A$
19	18	sselda	$⊢ ((F Fn A \land S \in P) \land y \in S) \to y \in A$
20	17 19	ffvelrnd	$⊢ ((F Fn A \land S \in P) \land y \in S) \to F (y) \in ran F$
21	14 20	eqeltrd	$⊢ ((F Fn A \land S \in P) \land y \in S) \to ⋃ F [S] \in ran F$
22	8 21	exlimddv	$⊢ (F Fn A \land S \in P) \to ⋃ F [S] \in ran F$

Metamath Proof Explorer

Theorem uniimaelsetpreimafv

Proof