This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ∪ ( ( 𝐹 “ { 𝐴 } ) ∪ ( 𝐺 “ { 𝐴 } ) ) = ( ( 𝐹 ‘ 𝐴 ) ∪ ( 𝐺 ‘ 𝐴 ) ) )
17 3 6 16 3eqtrd ⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( dom 𝐹 ∩ dom 𝐺 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) ∪ ( 𝐺 ‘ 𝐴 ) ) )