funiunfv

Description: The indexed union of a function's values is the union of its image under the index class.

Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to F Fn A , the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006) (Proof shortened by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	funiunfv	$⊢ Fun F \to ⋃_{x \in A} F (x) = ⋃ F [A]$

Proof

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
2	1	funfnd	$⊢ Fun F \to ({F ↾}_{A}) Fn dom ({F ↾}_{A})$
3		fniunfv	$⊢ ({F ↾}_{A}) Fn dom ({F ↾}_{A}) \to ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) = ⋃ ran ({F ↾}_{A})$
4	2 3	syl	$⊢ Fun F \to ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) = ⋃ ran ({F ↾}_{A})$
5		undif2	$⊢ dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A})) = dom ({F ↾}_{A}) \cup A$
6		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
7		inss1	$⊢ A \cap dom F \subseteq A$
8	6 7	eqsstri	$⊢ dom ({F ↾}_{A}) \subseteq A$
9		ssequn1	$⊢ dom ({F ↾}_{A}) \subseteq A \leftrightarrow dom ({F ↾}_{A}) \cup A = A$
10	8 9	mpbi	$⊢ dom ({F ↾}_{A}) \cup A = A$
11	5 10	eqtri	$⊢ dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A})) = A$
12		iuneq1	$⊢ dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A})) = A \to ⋃_{x \in dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A}))} ({F ↾}_{A}) (x) = ⋃_{x \in A} ({F ↾}_{A}) (x)$
13	11 12	ax-mp	$⊢ ⋃_{x \in dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A}))} ({F ↾}_{A}) (x) = ⋃_{x \in A} ({F ↾}_{A}) (x)$
14		iunxun	$⊢ ⋃_{x \in dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A}))} ({F ↾}_{A}) (x) = ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) \cup ⋃_{x \in A ∖ dom ({F ↾}_{A})} ({F ↾}_{A}) (x)$
15		eldifn	$⊢ x \in (A ∖ dom ({F ↾}_{A})) \to \neg x \in dom ({F ↾}_{A})$
16		ndmfv	$⊢ \neg x \in dom ({F ↾}_{A}) \to ({F ↾}_{A}) (x) = \emptyset$
17	15 16	syl	$⊢ x \in (A ∖ dom ({F ↾}_{A})) \to ({F ↾}_{A}) (x) = \emptyset$
18	17	iuneq2i	$⊢ ⋃_{x \in A ∖ dom ({F ↾}_{A})} ({F ↾}_{A}) (x) = ⋃_{x \in A ∖ dom ({F ↾}_{A})} \emptyset$
19		iun0	$⊢ ⋃_{x \in A ∖ dom ({F ↾}_{A})} \emptyset = \emptyset$
20	18 19	eqtri	$⊢ ⋃_{x \in A ∖ dom ({F ↾}_{A})} ({F ↾}_{A}) (x) = \emptyset$
21	20	uneq2i	$⊢ ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) \cup ⋃_{x \in A ∖ dom ({F ↾}_{A})} ({F ↾}_{A}) (x) = ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) \cup \emptyset$
22		un0	$⊢ ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) \cup \emptyset = ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x)$
23	21 22	eqtri	$⊢ ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x) \cup ⋃_{x \in A ∖ dom ({F ↾}_{A})} ({F ↾}_{A}) (x) = ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x)$
24	14 23	eqtri	$⊢ ⋃_{x \in dom ({F ↾}_{A}) \cup (A ∖ dom ({F ↾}_{A}))} ({F ↾}_{A}) (x) = ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x)$
25		fvres	$⊢ x \in A \to ({F ↾}_{A}) (x) = F (x)$
26	25	iuneq2i	$⊢ ⋃_{x \in A} ({F ↾}_{A}) (x) = ⋃_{x \in A} F (x)$
27	13 24 26	3eqtr3ri	$⊢ ⋃_{x \in A} F (x) = ⋃_{x \in dom ({F ↾}_{A})} ({F ↾}_{A}) (x)$
28		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
29	28	unieqi	$⊢ ⋃ F [A] = ⋃ ran ({F ↾}_{A})$
30	4 27 29	3eqtr4g	$⊢ Fun F \to ⋃_{x \in A} F (x) = ⋃ F [A]$

Metamath Proof Explorer

Theorem funiunfv

Proof