Metamath Proof Explorer

Theorem fun

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

Ref Expression
Assertion fun 
|- ( ( ( F : A --> C /\ G : B --> D ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) : ( A u. B ) --> ( C u. D ) )

Proof

Step Hyp Ref Expression
1 fnun 
 |-  ( ( ( F Fn A /\ G Fn B ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) )
2 1 expcom 
 |-  ( ( A i^i B ) = (/) -> ( ( F Fn A /\ G Fn B ) -> ( F u. G ) Fn ( A u. B ) ) )
3 rnun 
 |-  ran ( F u. G ) = ( ran F u. ran G )
4 unss12 
 |-  ( ( ran F C_ C /\ ran G C_ D ) -> ( ran F u. ran G ) C_ ( C u. D ) )
5 3 4 eqsstrid 
 |-  ( ( ran F C_ C /\ ran G C_ D ) -> ran ( F u. G ) C_ ( C u. D ) )
6 2 5 anim12d1 
 |-  ( ( A i^i B ) = (/) -> ( ( ( F Fn A /\ G Fn B ) /\ ( ran F C_ C /\ ran G C_ D ) ) -> ( ( F u. G ) Fn ( A u. B ) /\ ran ( F u. G ) C_ ( C u. D ) ) ) )
7 df-f 
 |-  ( F : A --> C <-> ( F Fn A /\ ran F C_ C ) )
8 df-f 
 |-  ( G : B --> D <-> ( G Fn B /\ ran G C_ D ) )
9 7 8 anbi12i 
 |-  ( ( F : A --> C /\ G : B --> D ) <-> ( ( F Fn A /\ ran F C_ C ) /\ ( G Fn B /\ ran G C_ D ) ) )
10 an4 
 |-  ( ( ( F Fn A /\ ran F C_ C ) /\ ( G Fn B /\ ran G C_ D ) ) <-> ( ( F Fn A /\ G Fn B ) /\ ( ran F C_ C /\ ran G C_ D ) ) )
11 9 10 bitri 
 |-  ( ( F : A --> C /\ G : B --> D ) <-> ( ( F Fn A /\ G Fn B ) /\ ( ran F C_ C /\ ran G C_ D ) ) )
12 df-f 
 |-  ( ( F u. G ) : ( A u. B ) --> ( C u. D ) <-> ( ( F u. G ) Fn ( A u. B ) /\ ran ( F u. G ) C_ ( C u. D ) ) )
13 6 11 12 3imtr4g 
 |-  ( ( A i^i B ) = (/) -> ( ( F : A --> C /\ G : B --> D ) -> ( F u. G ) : ( A u. B ) --> ( C u. D ) ) )
14 13 impcom 
 |-  ( ( ( F : A --> C /\ G : B --> D ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) : ( A u. B ) --> ( C u. D ) )