# Metamath Proof Explorer

## 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 ${⊢}\mathrm{Fun}{F}\to \bigcup _{{x}\in {A}}{F}\left({x}\right)=\bigcup {F}\left[{A}\right]$

### Proof

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