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

Metamath Proof Explorer

Theorem f1un

Description: The union of two one-to-one functions with disjoint domains and codomains. (Contributed by BTernaryTau, 3-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
2 1 frnd 
 |-  ( F : A -1-1-> B -> ran F C_ B )
3 f1f 
 |-  ( G : C -1-1-> D -> G : C --> D )
4 3 frnd 
 |-  ( G : C -1-1-> D -> ran G C_ D )
5 unss12 
 |-  ( ( ran F C_ B /\ ran G C_ D ) -> ( ran F u. ran G ) C_ ( B u. D ) )
6 2 4 5 syl2an 
 |-  ( ( F : A -1-1-> B /\ G : C -1-1-> D ) -> ( ran F u. ran G ) C_ ( B u. D ) )
7 f1f1orn 
 |-  ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
8 f1f1orn 
 |-  ( G : C -1-1-> D -> G : C -1-1-onto-> ran G )
9 7 8 anim12i 
 |-  ( ( F : A -1-1-> B /\ G : C -1-1-> D ) -> ( F : A -1-1-onto-> ran F /\ G : C -1-1-onto-> ran G ) )
10 simprl 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( A i^i C ) = (/) )
11 ss2in 
 |-  ( ( ran F C_ B /\ ran G C_ D ) -> ( ran F i^i ran G ) C_ ( B i^i D ) )
12 2 4 11 syl2an 
 |-  ( ( F : A -1-1-> B /\ G : C -1-1-> D ) -> ( ran F i^i ran G ) C_ ( B i^i D ) )
13 sseq0 
 |-  ( ( ( ran F i^i ran G ) C_ ( B i^i D ) /\ ( B i^i D ) = (/) ) -> ( ran F i^i ran G ) = (/) )
14 12 13 sylan 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( B i^i D ) = (/) ) -> ( ran F i^i ran G ) = (/) )
15 14 adantrl 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( ran F i^i ran G ) = (/) )
16 10 15 jca 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( ( A i^i C ) = (/) /\ ( ran F i^i ran G ) = (/) ) )
17 f1oun 
 |-  ( ( ( F : A -1-1-onto-> ran F /\ G : C -1-1-onto-> ran G ) /\ ( ( A i^i C ) = (/) /\ ( ran F i^i ran G ) = (/) ) ) -> ( F u. G ) : ( A u. C ) -1-1-onto-> ( ran F u. ran G ) )
18 9 16 17 syl2an2r 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( F u. G ) : ( A u. C ) -1-1-onto-> ( ran F u. ran G ) )
19 f1of1 
 |-  ( ( F u. G ) : ( A u. C ) -1-1-onto-> ( ran F u. ran G ) -> ( F u. G ) : ( A u. C ) -1-1-> ( ran F u. ran G ) )
20 18 19 syl 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( F u. G ) : ( A u. C ) -1-1-> ( ran F u. ran G ) )
21 f1ss 
 |-  ( ( ( F u. G ) : ( A u. C ) -1-1-> ( ran F u. ran G ) /\ ( ran F u. ran G ) C_ ( B u. D ) ) -> ( F u. G ) : ( A u. C ) -1-1-> ( B u. D ) )
22 21 ancoms 
 |-  ( ( ( ran F u. ran G ) C_ ( B u. D ) /\ ( F u. G ) : ( A u. C ) -1-1-> ( ran F u. ran G ) ) -> ( F u. G ) : ( A u. C ) -1-1-> ( B u. D ) )
23 6 20 22 syl2an2r 
 |-  ( ( ( F : A -1-1-> B /\ G : C -1-1-> D ) /\ ( ( A i^i C ) = (/) /\ ( B i^i D ) = (/) ) ) -> ( F u. G ) : ( A u. C ) -1-1-> ( B u. D ) )