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