Metamath Proof Explorer

Theorem foun

Description: The union of two onto functions with disjoint domains is an onto function. (Contributed by Mario Carneiro, 22-Jun-2016)

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

Proof

Step Hyp Ref Expression
1 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
2 fofn 
 |-  ( G : C -onto-> D -> G Fn C )
3 1 2 anim12i 
 |-  ( ( F : A -onto-> B /\ G : C -onto-> D ) -> ( F Fn A /\ G Fn C ) )
4 fnun 
 |-  ( ( ( F Fn A /\ G Fn C ) /\ ( A i^i C ) = (/) ) -> ( F u. G ) Fn ( A u. C ) )
5 3 4 sylan 
 |-  ( ( ( F : A -onto-> B /\ G : C -onto-> D ) /\ ( A i^i C ) = (/) ) -> ( F u. G ) Fn ( A u. C ) )
6 rnun 
 |-  ran ( F u. G ) = ( ran F u. ran G )
7 forn 
 |-  ( F : A -onto-> B -> ran F = B )
8 7 ad2antrr 
 |-  ( ( ( F : A -onto-> B /\ G : C -onto-> D ) /\ ( A i^i C ) = (/) ) -> ran F = B )
9 forn 
 |-  ( G : C -onto-> D -> ran G = D )
10 9 ad2antlr 
 |-  ( ( ( F : A -onto-> B /\ G : C -onto-> D ) /\ ( A i^i C ) = (/) ) -> ran G = D )
11 8 10 uneq12d 
 |-  ( ( ( F : A -onto-> B /\ G : C -onto-> D ) /\ ( A i^i C ) = (/) ) -> ( ran F u. ran G ) = ( B u. D ) )
12 6 11 syl5eq 
 |-  ( ( ( F : A -onto-> B /\ G : C -onto-> D ) /\ ( A i^i C ) = (/) ) -> ran ( F u. G ) = ( B u. D ) )
13 df-fo 
 |-  ( ( F u. G ) : ( A u. C ) -onto-> ( B u. D ) <-> ( ( F u. G ) Fn ( A u. C ) /\ ran ( F u. G ) = ( B u. D ) ) )
14 5 12 13 sylanbrc 
 |-  ( ( ( F : A -onto-> B /\ G : C -onto-> D ) /\ ( A i^i C ) = (/) ) -> ( F u. G ) : ( A u. C ) -onto-> ( B u. D ) )