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 𝐺 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ‘ 𝐴 ) = ( ( 𝐹 ‘ 𝐴 ) ∪ ( 𝐺 ‘ 𝐴 ) ) )