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 
|- ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( ( F u. G ) ` X ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( F Fn A -> Fun F )
2 1 3ad2ant1 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> Fun F )
3 fnfun 
 |-  ( G Fn B -> Fun G )
4 3 3ad2ant2 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> Fun G )
5 fndm 
 |-  ( F Fn A -> dom F = A )
6 fndm 
 |-  ( G Fn B -> dom G = B )
7 5 6 ineqan12d 
 |-  ( ( F Fn A /\ G Fn B ) -> ( dom F i^i dom G ) = ( A i^i B ) )
8 7 eqeq1d 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( dom F i^i dom G ) = (/) <-> ( A i^i B ) = (/) ) )
9 8 biimprd 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( A i^i B ) = (/) -> ( dom F i^i dom G ) = (/) ) )
10 9 adantrd 
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( ( A i^i B ) = (/) /\ X e. A ) -> ( dom F i^i dom G ) = (/) ) )
11 10 3impia 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( dom F i^i dom G ) = (/) )
12 fvun 
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> ( ( F u. G ) ` X ) = ( ( F ` X ) u. ( G ` X ) ) )
13 2 4 11 12 syl21anc 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( ( F u. G ) ` X ) = ( ( F ` X ) u. ( G ` X ) ) )
14 disjel 
 |-  ( ( ( A i^i B ) = (/) /\ X e. A ) -> -. X e. B )
15 14 adantl 
 |-  ( ( G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> -. X e. B )
16 6 eleq2d 
 |-  ( G Fn B -> ( X e. dom G <-> X e. B ) )
17 16 adantr 
 |-  ( ( G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( X e. dom G <-> X e. B ) )
18 15 17 mtbird 
 |-  ( ( G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> -. X e. dom G )
19 18 3adant1 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> -. X e. dom G )
20 ndmfv 
 |-  ( -. X e. dom G -> ( G ` X ) = (/) )
21 19 20 syl 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( G ` X ) = (/) )
22 21 uneq2d 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( ( F ` X ) u. ( G ` X ) ) = ( ( F ` X ) u. (/) ) )
23 un0 
 |-  ( ( F ` X ) u. (/) ) = ( F ` X )
24 22 23 eqtrdi 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( ( F ` X ) u. ( G ` X ) ) = ( F ` X ) )
25 13 24 eqtrd 
 |-  ( ( F Fn A /\ G Fn B /\ ( ( A i^i B ) = (/) /\ X e. A ) ) -> ( ( F u. G ) ` X ) = ( F ` X ) )