Theorem 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 -> U_ x e. A ( F ` x ) = U. ( F " A ) )

Proof

Step	Hyp	Ref	Expression
1		funres	|- ( Fun F -> Fun ( F |` A ) )
2	1	funfnd	|- ( Fun F -> ( F |` A ) Fn dom ( F |` A ) )
3		fniunfv	|- ( ( F |` A ) Fn dom ( F |` A ) -> U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) = U. ran ( F |` A ) )
4	2 3	syl	|- ( Fun F -> U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) = U. ran ( F |` A ) )
5		undif2	|- ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) = ( dom ( F |` A ) u. A )
6		dmres	|- dom ( F |` A ) = ( A i^i dom F )
7		inss1	|- ( A i^i dom F ) C_ A
8	6 7	eqsstri	|- dom ( F |` A ) C_ A
9		ssequn1	|- ( dom ( F |` A ) C_ A <-> ( dom ( F |` A ) u. A ) = A )
10	8 9	mpbi	|- ( dom ( F |` A ) u. A ) = A
11	5 10	eqtri	|- ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) = A
12		iuneq1	|- ( ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) = A -> U_ x e. ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) ( ( F |` A ) ` x ) = U_ x e. A ( ( F |` A ) ` x ) )
13	11 12	ax-mp	|- U_ x e. ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) ( ( F |` A ) ` x ) = U_ x e. A ( ( F |` A ) ` x )
14		iunxun	|- U_ x e. ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) ( ( F |` A ) ` x ) = ( U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) u. U_ x e. ( A \ dom ( F |` A ) ) ( ( F |` A ) ` x ) )
15		eldifn	|- ( x e. ( A \ dom ( F |` A ) ) -> -. x e. dom ( F |` A ) )
16		ndmfv	|- ( -. x e. dom ( F |` A ) -> ( ( F |` A ) ` x ) = (/) )
17	15 16	syl	|- ( x e. ( A \ dom ( F |` A ) ) -> ( ( F |` A ) ` x ) = (/) )
18	17	iuneq2i	|- U_ x e. ( A \ dom ( F |` A ) ) ( ( F |` A ) ` x ) = U_ x e. ( A \ dom ( F |` A ) ) (/)
19		iun0	|- U_ x e. ( A \ dom ( F |` A ) ) (/) = (/)
20	18 19	eqtri	|- U_ x e. ( A \ dom ( F |` A ) ) ( ( F |` A ) ` x ) = (/)
21	20	uneq2i	|- ( U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) u. U_ x e. ( A \ dom ( F |` A ) ) ( ( F |` A ) ` x ) ) = ( U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) u. (/) )
22		un0	|- ( U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) u. (/) ) = U_ x e. dom ( F |` A ) ( ( F |` A ) ` x )
23	21 22	eqtri	|- ( U_ x e. dom ( F |` A ) ( ( F |` A ) ` x ) u. U_ x e. ( A \ dom ( F |` A ) ) ( ( F |` A ) ` x ) ) = U_ x e. dom ( F |` A ) ( ( F |` A ) ` x )
24	14 23	eqtri	|- U_ x e. ( dom ( F |` A ) u. ( A \ dom ( F |` A ) ) ) ( ( F |` A ) ` x ) = U_ x e. dom ( F |` A ) ( ( F |` A ) ` x )
25		fvres	|- ( x e. A -> ( ( F |` A ) ` x ) = ( F ` x ) )
26	25	iuneq2i	|- U_ x e. A ( ( F |` A ) ` x ) = U_ x e. A ( F ` x )
27	13 24 26	3eqtr3ri	|- U_ x e. A ( F ` x ) = U_ x e. dom ( F |` A ) ( ( F |` A ) ` x )
28		df-ima	|- ( F " A ) = ran ( F |` A )
29	28	unieqi	|- U. ( F " A ) = U. ran ( F |` A )
30	4 27 29	3eqtr4g	|- ( Fun F -> U_ x e. A ( F ` x ) = U. ( F " A ) )