Step |
Hyp |
Ref |
Expression |
1 |
|
dffo2 |
|- ( F : B -onto-> C <-> ( F : B --> C /\ ran F = C ) ) |
2 |
|
dffo2 |
|- ( G : A -onto-> B <-> ( G : A --> B /\ ran G = B ) ) |
3 |
|
fco |
|- ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C ) |
4 |
3
|
ad2ant2r |
|- ( ( ( F : B --> C /\ ran F = C ) /\ ( G : A --> B /\ ran G = B ) ) -> ( F o. G ) : A --> C ) |
5 |
|
fdm |
|- ( F : B --> C -> dom F = B ) |
6 |
|
eqtr3 |
|- ( ( dom F = B /\ ran G = B ) -> dom F = ran G ) |
7 |
5 6
|
sylan |
|- ( ( F : B --> C /\ ran G = B ) -> dom F = ran G ) |
8 |
|
rncoeq |
|- ( dom F = ran G -> ran ( F o. G ) = ran F ) |
9 |
8
|
eqeq1d |
|- ( dom F = ran G -> ( ran ( F o. G ) = C <-> ran F = C ) ) |
10 |
9
|
biimpar |
|- ( ( dom F = ran G /\ ran F = C ) -> ran ( F o. G ) = C ) |
11 |
7 10
|
sylan |
|- ( ( ( F : B --> C /\ ran G = B ) /\ ran F = C ) -> ran ( F o. G ) = C ) |
12 |
11
|
an32s |
|- ( ( ( F : B --> C /\ ran F = C ) /\ ran G = B ) -> ran ( F o. G ) = C ) |
13 |
12
|
adantrl |
|- ( ( ( F : B --> C /\ ran F = C ) /\ ( G : A --> B /\ ran G = B ) ) -> ran ( F o. G ) = C ) |
14 |
4 13
|
jca |
|- ( ( ( F : B --> C /\ ran F = C ) /\ ( G : A --> B /\ ran G = B ) ) -> ( ( F o. G ) : A --> C /\ ran ( F o. G ) = C ) ) |
15 |
1 2 14
|
syl2anb |
|- ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( ( F o. G ) : A --> C /\ ran ( F o. G ) = C ) ) |
16 |
|
dffo2 |
|- ( ( F o. G ) : A -onto-> C <-> ( ( F o. G ) : A --> C /\ ran ( F o. G ) = C ) ) |
17 |
15 16
|
sylibr |
|- ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : A -onto-> C ) |