# Metamath Proof Explorer

## Theorem fvun

Description: Value of the union of two functions when the domains are separate. (Contributed by FL, 7-Nov-2011)

Ref Expression
Assertion fvun ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left({F}\cup {G}\right)\left({A}\right)={F}\left({A}\right)\cup {G}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 funun ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \mathrm{Fun}\left({F}\cup {G}\right)$
2 funfv ${⊢}\mathrm{Fun}\left({F}\cup {G}\right)\to \left({F}\cup {G}\right)\left({A}\right)=\bigcup \left({F}\cup {G}\right)\left[\left\{{A}\right\}\right]$
3 1 2 syl ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left({F}\cup {G}\right)\left({A}\right)=\bigcup \left({F}\cup {G}\right)\left[\left\{{A}\right\}\right]$
4 imaundir ${⊢}\left({F}\cup {G}\right)\left[\left\{{A}\right\}\right]={F}\left[\left\{{A}\right\}\right]\cup {G}\left[\left\{{A}\right\}\right]$
5 4 a1i ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left({F}\cup {G}\right)\left[\left\{{A}\right\}\right]={F}\left[\left\{{A}\right\}\right]\cup {G}\left[\left\{{A}\right\}\right]$
6 5 unieqd ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \bigcup \left({F}\cup {G}\right)\left[\left\{{A}\right\}\right]=\bigcup \left({F}\left[\left\{{A}\right\}\right]\cup {G}\left[\left\{{A}\right\}\right]\right)$
7 uniun ${⊢}\bigcup \left({F}\left[\left\{{A}\right\}\right]\cup {G}\left[\left\{{A}\right\}\right]\right)=\bigcup {F}\left[\left\{{A}\right\}\right]\cup \bigcup {G}\left[\left\{{A}\right\}\right]$
8 funfv ${⊢}\mathrm{Fun}{F}\to {F}\left({A}\right)=\bigcup {F}\left[\left\{{A}\right\}\right]$
9 8 eqcomd ${⊢}\mathrm{Fun}{F}\to \bigcup {F}\left[\left\{{A}\right\}\right]={F}\left({A}\right)$
10 funfv ${⊢}\mathrm{Fun}{G}\to {G}\left({A}\right)=\bigcup {G}\left[\left\{{A}\right\}\right]$
11 10 eqcomd ${⊢}\mathrm{Fun}{G}\to \bigcup {G}\left[\left\{{A}\right\}\right]={G}\left({A}\right)$
12 9 11 anim12i ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\to \left(\bigcup {F}\left[\left\{{A}\right\}\right]={F}\left({A}\right)\wedge \bigcup {G}\left[\left\{{A}\right\}\right]={G}\left({A}\right)\right)$
13 12 adantr ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left(\bigcup {F}\left[\left\{{A}\right\}\right]={F}\left({A}\right)\wedge \bigcup {G}\left[\left\{{A}\right\}\right]={G}\left({A}\right)\right)$
14 uneq12 ${⊢}\left(\bigcup {F}\left[\left\{{A}\right\}\right]={F}\left({A}\right)\wedge \bigcup {G}\left[\left\{{A}\right\}\right]={G}\left({A}\right)\right)\to \bigcup {F}\left[\left\{{A}\right\}\right]\cup \bigcup {G}\left[\left\{{A}\right\}\right]={F}\left({A}\right)\cup {G}\left({A}\right)$
15 13 14 syl ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \bigcup {F}\left[\left\{{A}\right\}\right]\cup \bigcup {G}\left[\left\{{A}\right\}\right]={F}\left({A}\right)\cup {G}\left({A}\right)$
16 7 15 syl5eq ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \bigcup \left({F}\left[\left\{{A}\right\}\right]\cup {G}\left[\left\{{A}\right\}\right]\right)={F}\left({A}\right)\cup {G}\left({A}\right)$
17 3 6 16 3eqtrd ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\right)\wedge \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)\to \left({F}\cup {G}\right)\left({A}\right)={F}\left({A}\right)\cup {G}\left({A}\right)$