# Metamath Proof Explorer

## Theorem fvun1

Description: The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013)

Ref Expression
Assertion fvun1 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \left({F}\cup {G}\right)\left({X}\right)={F}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 fnfun ${⊢}{F}Fn{A}\to \mathrm{Fun}{F}$
2 1 3ad2ant1 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \mathrm{Fun}{F}$
3 fnfun ${⊢}{G}Fn{B}\to \mathrm{Fun}{G}$
4 3 3ad2ant2 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \mathrm{Fun}{G}$
5 fndm ${⊢}{F}Fn{A}\to \mathrm{dom}{F}={A}$
6 fndm ${⊢}{G}Fn{B}\to \mathrm{dom}{G}={B}$
7 5 6 ineqan12d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \mathrm{dom}{F}\cap \mathrm{dom}{G}={A}\cap {B}$
8 7 eqeq1d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left(\mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing ↔{A}\cap {B}=\varnothing \right)$
9 8 biimprd ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left({A}\cap {B}=\varnothing \to \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)$
10 9 adantrd ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\right)\to \left(\left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\to \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing \right)$
11 10 3impia ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \mathrm{dom}{F}\cap \mathrm{dom}{G}=\varnothing$
12 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({X}\right)={F}\left({X}\right)\cup {G}\left({X}\right)$
13 2 4 11 12 syl21anc ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \left({F}\cup {G}\right)\left({X}\right)={F}\left({X}\right)\cup {G}\left({X}\right)$
14 disjel ${⊢}\left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\to ¬{X}\in {B}$
15 14 adantl ${⊢}\left({G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to ¬{X}\in {B}$
16 6 eleq2d ${⊢}{G}Fn{B}\to \left({X}\in \mathrm{dom}{G}↔{X}\in {B}\right)$
17 16 adantr ${⊢}\left({G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \left({X}\in \mathrm{dom}{G}↔{X}\in {B}\right)$
18 15 17 mtbird ${⊢}\left({G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to ¬{X}\in \mathrm{dom}{G}$
19 18 3adant1 ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to ¬{X}\in \mathrm{dom}{G}$
20 ndmfv ${⊢}¬{X}\in \mathrm{dom}{G}\to {G}\left({X}\right)=\varnothing$
21 19 20 syl ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to {G}\left({X}\right)=\varnothing$
22 21 uneq2d ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to {F}\left({X}\right)\cup {G}\left({X}\right)={F}\left({X}\right)\cup \varnothing$
23 un0 ${⊢}{F}\left({X}\right)\cup \varnothing ={F}\left({X}\right)$
24 22 23 syl6eq ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to {F}\left({X}\right)\cup {G}\left({X}\right)={F}\left({X}\right)$
25 13 24 eqtrd ${⊢}\left({F}Fn{A}\wedge {G}Fn{B}\wedge \left({A}\cap {B}=\varnothing \wedge {X}\in {A}\right)\right)\to \left({F}\cup {G}\right)\left({X}\right)={F}\left({X}\right)$