Metamath Proof Explorer

Theorem f1oun

Description: The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998)

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

Proof

Step Hyp Ref Expression
1 dff1o4 
 |-  ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )
2 dff1o4 
 |-  ( G : C -1-1-onto-> D <-> ( G Fn C /\ `' G Fn D ) )
3 fnun 
 |-  ( ( ( F Fn A /\ G Fn C ) /\ ( A i^i C ) = (/) ) -> ( F u. G ) Fn ( A u. C ) )
4 3 ex 
 |-  ( ( F Fn A /\ G Fn C ) -> ( ( A i^i C ) = (/) -> ( F u. G ) Fn ( A u. C ) ) )
5 fnun 
 |-  ( ( ( `' F Fn B /\ `' G Fn D ) /\ ( B i^i D ) = (/) ) -> ( `' F u. `' G ) Fn ( B u. D ) )
6 cnvun 
 |-  `' ( F u. G ) = ( `' F u. `' G )
7 6 fneq1i 
 |-  ( `' ( F u. G ) Fn ( B u. D ) <-> ( `' F u. `' G ) Fn ( B u. D ) )
8 5 7 sylibr 
 |-  ( ( ( `' F Fn B /\ `' G Fn D ) /\ ( B i^i D ) = (/) ) -> `' ( F u. G ) Fn ( B u. D ) )
9 8 ex 
 |-  ( ( `' F Fn B /\ `' G Fn D ) -> ( ( B i^i D ) = (/) -> `' ( F u. G ) Fn ( B u. D ) ) )
10 4 9 im2anan9 
 |-  ( ( ( F Fn A /\ G Fn C ) /\ ( `' F Fn B /\ `' G Fn D ) ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( ( F u. G ) Fn ( A u. C ) /\ `' ( F u. G ) Fn ( B u. D ) ) ) )
11 10 an4s 
 |-  ( ( ( F Fn A /\ `' F Fn B ) /\ ( G Fn C /\ `' G Fn D ) ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( ( F u. G ) Fn ( A u. C ) /\ `' ( F u. G ) Fn ( B u. D ) ) ) )
12 1 2 11 syl2anb 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( ( F u. G ) Fn ( A u. C ) /\ `' ( F u. G ) Fn ( B u. D ) ) ) )
13 dff1o4 
 |-  ( ( F u. G ) : ( A u. C ) -1-1-onto-> ( B u. D ) <-> ( ( F u. G ) Fn ( A u. C ) /\ `' ( F u. G ) Fn ( B u. D ) ) )
14 12 13 syl6ibr 
 |-  ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D ) -> ( ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) -> ( F u. G ) : ( A u. C ) -1-1-onto-> ( B u. D ) ) )
15 14 imp 
 |-  ( ( ( F : A -1-1-onto-> B /\ G : C -1-1-onto-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( F u. G ) : ( A u. C ) -1-1-onto-> ( B u. D ) )