| 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 |
1
|
ffnd |
|- ( ph -> F Fn A ) |
| 6 |
2
|
a1i |
|- ( ph -> E = ( ran F i^i C ) ) |
| 7 |
3
|
a1i |
|- ( ph -> P = ( `' F " C ) ) |
| 8 |
5 6 7
|
rescnvimafod |
|- ( ph -> ( F |` P ) : P -onto-> E ) |
| 9 |
|
foeq1 |
|- ( X = ( F |` P ) -> ( X : P -onto-> E <-> ( F |` P ) : P -onto-> E ) ) |
| 10 |
4 9
|
mp1i |
|- ( ph -> ( X : P -onto-> E <-> ( F |` P ) : P -onto-> E ) ) |
| 11 |
8 10
|
mpbird |
|- ( ph -> X : P -onto-> E ) |