# 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 ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹𝐺 ) ‘ 𝐴 ) = ( ( 𝐹𝐴 ) ∪ ( 𝐺𝐴 ) ) )

### Proof

Step Hyp Ref Expression
1 funun ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → Fun ( 𝐹𝐺 ) )
2 funfv ( Fun ( 𝐹𝐺 ) → ( ( 𝐹𝐺 ) ‘ 𝐴 ) = ( ( 𝐹𝐺 ) “ { 𝐴 } ) )
3 1 2 syl ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹𝐺 ) ‘ 𝐴 ) = ( ( 𝐹𝐺 ) “ { 𝐴 } ) )
4 imaundir ( ( 𝐹𝐺 ) “ { 𝐴 } ) = ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) )
5 4 a1i ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹𝐺 ) “ { 𝐴 } ) = ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) )
6 5 unieqd ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹𝐺 ) “ { 𝐴 } ) = ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) )
7 uniun ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) = ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) )
8 funfv ( Fun 𝐹 → ( 𝐹𝐴 ) = ( 𝐹 “ { 𝐴 } ) )
9 8 eqcomd ( Fun 𝐹 ( 𝐹 “ { 𝐴 } ) = ( 𝐹𝐴 ) )
10 funfv ( Fun 𝐺 → ( 𝐺𝐴 ) = ( 𝐺 “ { 𝐴 } ) )
11 10 eqcomd ( Fun 𝐺 ( 𝐺 “ { 𝐴 } ) = ( 𝐺𝐴 ) )
12 9 11 anim12i ( ( Fun 𝐹 ∧ Fun 𝐺 ) → ( ( 𝐹 “ { 𝐴 } ) = ( 𝐹𝐴 ) ∧ ( 𝐺 “ { 𝐴 } ) = ( 𝐺𝐴 ) ) )
13 12 adantr ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 “ { 𝐴 } ) = ( 𝐹𝐴 ) ∧ ( 𝐺 “ { 𝐴 } ) = ( 𝐺𝐴 ) ) )
14 uneq12 ( ( ( 𝐹 “ { 𝐴 } ) = ( 𝐹𝐴 ) ∧ ( 𝐺 “ { 𝐴 } ) = ( 𝐺𝐴 ) ) → ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) = ( ( 𝐹𝐴 ) ∪ ( 𝐺𝐴 ) ) )
15 13 14 syl ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) = ( ( 𝐹𝐴 ) ∪ ( 𝐺𝐴 ) ) )
16 7 15 syl5eq ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) = ( ( 𝐹𝐴 ) ∪ ( 𝐺𝐴 ) ) )
17 3 6 16 3eqtrd ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹𝐺 ) ‘ 𝐴 ) = ( ( 𝐹𝐴 ) ∪ ( 𝐺𝐴 ) ) )