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 F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) ` A ) = ( ( F ` A ) u. ( G ` A ) ) )

Proof

Step Hyp Ref Expression
1 funun 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )
2 funfv 
 |-  ( Fun ( F u. G ) -> ( ( F u. G ) ` A ) = U. ( ( F u. G ) " { A } ) )
3 1 2 syl 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) ` A ) = U. ( ( F u. G ) " { A } ) )
4 imaundir 
 |-  ( ( F u. G ) " { A } ) = ( ( F " { A } ) u. ( G " { A } ) )
5 4 a1i 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) " { A } ) = ( ( F " { A } ) u. ( G " { A } ) ) )
6 5 unieqd 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> U. ( ( F u. G ) " { A } ) = U. ( ( F " { A } ) u. ( G " { A } ) ) )
7 uniun 
 |-  U. ( ( F " { A } ) u. ( G " { A } ) ) = ( U. ( F " { A } ) u. U. ( G " { A } ) )
8 funfv 
 |-  ( Fun F -> ( F ` A ) = U. ( F " { A } ) )
9 8 eqcomd 
 |-  ( Fun F -> U. ( F " { A } ) = ( F ` A ) )
10 funfv 
 |-  ( Fun G -> ( G ` A ) = U. ( G " { A } ) )
11 10 eqcomd 
 |-  ( Fun G -> U. ( G " { A } ) = ( G ` A ) )
12 9 11 anim12i 
 |-  ( ( Fun F /\ Fun G ) -> ( U. ( F " { A } ) = ( F ` A ) /\ U. ( G " { A } ) = ( G ` A ) ) )
13 12 adantr 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( U. ( F " { A } ) = ( F ` A ) /\ U. ( G " { A } ) = ( G ` A ) ) )
14 uneq12 
 |-  ( ( U. ( F " { A } ) = ( F ` A ) /\ U. ( G " { A } ) = ( G ` A ) ) -> ( U. ( F " { A } ) u. U. ( G " { A } ) ) = ( ( F ` A ) u. ( G ` A ) ) )
15 13 14 syl 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( U. ( F " { A } ) u. U. ( G " { A } ) ) = ( ( F ` A ) u. ( G ` A ) ) )
16 7 15 eqtrid 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> U. ( ( F " { A } ) u. ( G " { A } ) ) = ( ( F ` A ) u. ( G ` A ) ) )
17 3 6 16 3eqtrd 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) ` A ) = ( ( F ` A ) u. ( G ` A ) ) )