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