| 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 |
5
|
ffnd |
|- ( ph -> G Fn C ) |
| 8 |
2
|
a1i |
|- ( ph -> E = ( ran F i^i C ) ) |
| 9 |
|
inss2 |
|- ( ran F i^i C ) C_ C |
| 10 |
8 9
|
eqsstrdi |
|- ( ph -> E C_ C ) |
| 11 |
7 10
|
fnssresd |
|- ( ph -> ( G |` E ) Fn E ) |
| 12 |
6
|
fneq1i |
|- ( Y Fn E <-> ( G |` E ) Fn E ) |
| 13 |
11 12
|
sylibr |
|- ( ph -> Y Fn E ) |
| 14 |
1 2 3 4
|
fcoreslem3 |
|- ( ph -> X : P -onto-> E ) |
| 15 |
|
fofn |
|- ( X : P -onto-> E -> X Fn P ) |
| 16 |
14 15
|
syl |
|- ( ph -> X Fn P ) |
| 17 |
1 2 3 4
|
fcoreslem2 |
|- ( ph -> ran X = E ) |
| 18 |
|
eqimss |
|- ( ran X = E -> ran X C_ E ) |
| 19 |
17 18
|
syl |
|- ( ph -> ran X C_ E ) |
| 20 |
|
fnco |
|- ( ( Y Fn E /\ X Fn P /\ ran X C_ E ) -> ( Y o. X ) Fn P ) |
| 21 |
13 16 19 20
|
syl3anc |
|- ( ph -> ( Y o. X ) Fn P ) |