| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fcores.f |
|- ( ph -> F : A --> B ) |
| 2 |
|
fcores.e |
|- E = ( ran F i^i C ) |
| 3 |
|
fcores.p |
|- P = ( `' F " C ) |
| 4 |
|
fcores.x |
|- X = ( F |` P ) |
| 5 |
|
fcores.g |
|- ( ph -> G : C --> D ) |
| 6 |
|
fcores.y |
|- Y = ( G |` E ) |
| 7 |
1 2 3 4 5 6
|
fcores |
|- ( ph -> ( G o. F ) = ( Y o. X ) ) |
| 8 |
7
|
fveq1d |
|- ( ph -> ( ( G o. F ) ` Z ) = ( ( Y o. X ) ` Z ) ) |
| 9 |
8
|
adantr |
|- ( ( ph /\ Z e. P ) -> ( ( G o. F ) ` Z ) = ( ( Y o. X ) ` Z ) ) |
| 10 |
1 2 3 4
|
fcoreslem3 |
|- ( ph -> X : P -onto-> E ) |
| 11 |
|
fof |
|- ( X : P -onto-> E -> X : P --> E ) |
| 12 |
10 11
|
syl |
|- ( ph -> X : P --> E ) |
| 13 |
12
|
adantr |
|- ( ( ph /\ Z e. P ) -> X : P --> E ) |
| 14 |
|
simpr |
|- ( ( ph /\ Z e. P ) -> Z e. P ) |
| 15 |
13 14
|
fvco3d |
|- ( ( ph /\ Z e. P ) -> ( ( Y o. X ) ` Z ) = ( Y ` ( X ` Z ) ) ) |
| 16 |
9 15
|
eqtrd |
|- ( ( ph /\ Z e. P ) -> ( ( G o. F ) ` Z ) = ( Y ` ( X ` Z ) ) ) |