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 ) )