Metamath Proof Explorer


Theorem fnun

Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004)

Ref Expression
Assertion fnun
|- ( ( ( F Fn A /\ G Fn B ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) )

Proof

Step Hyp Ref Expression
1 df-fn
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
2 df-fn
 |-  ( G Fn B <-> ( Fun G /\ dom G = B ) )
3 ineq12
 |-  ( ( dom F = A /\ dom G = B ) -> ( dom F i^i dom G ) = ( A i^i B ) )
4 3 eqeq1d
 |-  ( ( dom F = A /\ dom G = B ) -> ( ( dom F i^i dom G ) = (/) <-> ( A i^i B ) = (/) ) )
5 4 anbi2d
 |-  ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) <-> ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) ) )
6 funun
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )
7 5 6 syl6bir
 |-  ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) -> Fun ( F u. G ) ) )
8 dmun
 |-  dom ( F u. G ) = ( dom F u. dom G )
9 uneq12
 |-  ( ( dom F = A /\ dom G = B ) -> ( dom F u. dom G ) = ( A u. B ) )
10 8 9 eqtrid
 |-  ( ( dom F = A /\ dom G = B ) -> dom ( F u. G ) = ( A u. B ) )
11 7 10 jctird
 |-  ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) -> ( Fun ( F u. G ) /\ dom ( F u. G ) = ( A u. B ) ) ) )
12 df-fn
 |-  ( ( F u. G ) Fn ( A u. B ) <-> ( Fun ( F u. G ) /\ dom ( F u. G ) = ( A u. B ) ) )
13 11 12 syl6ibr
 |-  ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) ) )
14 13 expd
 |-  ( ( dom F = A /\ dom G = B ) -> ( ( Fun F /\ Fun G ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) ) )
15 14 impcom
 |-  ( ( ( Fun F /\ Fun G ) /\ ( dom F = A /\ dom G = B ) ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) )
16 15 an4s
 |-  ( ( ( Fun F /\ dom F = A ) /\ ( Fun G /\ dom G = B ) ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) )
17 1 2 16 syl2anb
 |-  ( ( F Fn A /\ G Fn B ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) )
18 17 imp
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) )