elunirn

Description: Membership in the union of the range of a function. See elunirnALT for a shorter proof which uses ax-pow . See elfvunirn for a more general version of the reverse direction. (Contributed by NM, 24-Sep-2006)

		Ref	Expression
	Assertion	elunirn	$⊢ Fun F \to (A \in ⋃ ran F \leftrightarrow \exists x \in dom F A \in F (x))$

Proof

Step	Hyp	Ref	Expression
1		eluni	$⊢ A \in ⋃ ran F \leftrightarrow \exists y (A \in y \land y \in ran F)$
2		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
3		fvelrnb	$⊢ F Fn dom F \to (y \in ran F \leftrightarrow \exists x \in dom F F (x) = y)$
4	2 3	sylbi	$⊢ Fun F \to (y \in ran F \leftrightarrow \exists x \in dom F F (x) = y)$
5	4	anbi2d	$⊢ Fun F \to ((A \in y \land y \in ran F) \leftrightarrow (A \in y \land \exists x \in dom F F (x) = y))$
6		r19.42v	$⊢ \exists x \in dom F (A \in y \land F (x) = y) \leftrightarrow (A \in y \land \exists x \in dom F F (x) = y)$
7	5 6	bitr4di	$⊢ Fun F \to ((A \in y \land y \in ran F) \leftrightarrow \exists x \in dom F (A \in y \land F (x) = y))$
8		eleq2	$⊢ F (x) = y \to (A \in F (x) \leftrightarrow A \in y)$
9	8	biimparc	$⊢ (A \in y \land F (x) = y) \to A \in F (x)$
10	9	reximi	$⊢ \exists x \in dom F (A \in y \land F (x) = y) \to \exists x \in dom F A \in F (x)$
11	7 10	biimtrdi	$⊢ Fun F \to ((A \in y \land y \in ran F) \to \exists x \in dom F A \in F (x))$
12	11	exlimdv	$⊢ Fun F \to (\exists y (A \in y \land y \in ran F) \to \exists x \in dom F A \in F (x))$
13		fvelrn	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
14	13	a1d	$⊢ (Fun F \land x \in dom F) \to (A \in F (x) \to F (x) \in ran F)$
15	14	ancld	$⊢ (Fun F \land x \in dom F) \to (A \in F (x) \to (A \in F (x) \land F (x) \in ran F))$
16		fvex	$⊢ F (x) \in V$
17		eleq2	$⊢ y = F (x) \to (A \in y \leftrightarrow A \in F (x))$
18		eleq1	$⊢ y = F (x) \to (y \in ran F \leftrightarrow F (x) \in ran F)$
19	17 18	anbi12d	$⊢ y = F (x) \to ((A \in y \land y \in ran F) \leftrightarrow (A \in F (x) \land F (x) \in ran F))$
20	16 19	spcev	$⊢ (A \in F (x) \land F (x) \in ran F) \to \exists y (A \in y \land y \in ran F)$
21	15 20	syl6	$⊢ (Fun F \land x \in dom F) \to (A \in F (x) \to \exists y (A \in y \land y \in ran F))$
22	21	rexlimdva	$⊢ Fun F \to (\exists x \in dom F A \in F (x) \to \exists y (A \in y \land y \in ran F))$
23	12 22	impbid	$⊢ Fun F \to (\exists y (A \in y \land y \in ran F) \leftrightarrow \exists x \in dom F A \in F (x))$
24	1 23	bitrid	$⊢ Fun F \to (A \in ⋃ ran F \leftrightarrow \exists x \in dom F A \in F (x))$

Metamath Proof Explorer

Theorem elunirn

Proof