# Metamath Proof Explorer

## Theorem fun

Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004)

Ref Expression
Assertion fun ${⊢}\left(\left({F}:{A}⟶{C}\wedge {G}:{B}⟶{D}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({F}\cup {G}\right):{A}\cup {B}⟶{C}\cup {D}$

### Proof

Step Hyp Ref Expression
1 fnun ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({F}\cup {G}\right)Fn\left({A}\cup {B}\right)$
2 1 expcom ${⊢}{A}\cap {B}=\varnothing \to \left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left({F}\cup {G}\right)Fn\left({A}\cup {B}\right)\right)$
3 rnun ${⊢}\mathrm{ran}\left({F}\cup {G}\right)=\mathrm{ran}{F}\cup \mathrm{ran}{G}$
4 unss12 ${⊢}\left(\mathrm{ran}{F}\subseteq {C}\wedge \mathrm{ran}{G}\subseteq {D}\right)\to \mathrm{ran}{F}\cup \mathrm{ran}{G}\subseteq {C}\cup {D}$
5 3 4 eqsstrid ${⊢}\left(\mathrm{ran}{F}\subseteq {C}\wedge \mathrm{ran}{G}\subseteq {D}\right)\to \mathrm{ran}\left({F}\cup {G}\right)\subseteq {C}\cup {D}$
6 2 5 anim12d1 ${⊢}{A}\cap {B}=\varnothing \to \left(\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left(\mathrm{ran}{F}\subseteq {C}\wedge \mathrm{ran}{G}\subseteq {D}\right)\right)\to \left(\left({F}\cup {G}\right)Fn\left({A}\cup {B}\right)\wedge \mathrm{ran}\left({F}\cup {G}\right)\subseteq {C}\cup {D}\right)\right)$
7 df-f ${⊢}{F}:{A}⟶{C}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {C}\right)$
8 df-f ${⊢}{G}:{B}⟶{D}↔\left({G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {D}\right)$
9 7 8 anbi12i ${⊢}\left({F}:{A}⟶{C}\wedge {G}:{B}⟶{D}\right)↔\left(\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {C}\right)\wedge \left({G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {D}\right)\right)$
10 an4 ${⊢}\left(\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {C}\right)\wedge \left({G}Fn{B}\wedge \mathrm{ran}{G}\subseteq {D}\right)\right)↔\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left(\mathrm{ran}{F}\subseteq {C}\wedge \mathrm{ran}{G}\subseteq {D}\right)\right)$
11 9 10 bitri ${⊢}\left({F}:{A}⟶{C}\wedge {G}:{B}⟶{D}\right)↔\left(\left({F}Fn{A}\wedge {G}Fn{B}\right)\wedge \left(\mathrm{ran}{F}\subseteq {C}\wedge \mathrm{ran}{G}\subseteq {D}\right)\right)$
12 df-f ${⊢}\left({F}\cup {G}\right):{A}\cup {B}⟶{C}\cup {D}↔\left(\left({F}\cup {G}\right)Fn\left({A}\cup {B}\right)\wedge \mathrm{ran}\left({F}\cup {G}\right)\subseteq {C}\cup {D}\right)$
13 6 11 12 3imtr4g ${⊢}{A}\cap {B}=\varnothing \to \left(\left({F}:{A}⟶{C}\wedge {G}:{B}⟶{D}\right)\to \left({F}\cup {G}\right):{A}\cup {B}⟶{C}\cup {D}\right)$
14 13 impcom ${⊢}\left(\left({F}:{A}⟶{C}\wedge {G}:{B}⟶{D}\right)\wedge {A}\cap {B}=\varnothing \right)\to \left({F}\cup {G}\right):{A}\cup {B}⟶{C}\cup {D}$