This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrdi 
 |-  ( ( 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 imbitrrdi 
 |-  ( ( 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 ) )