| 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 |
|
df-ima |
|- ( F " P ) = ran ( F |` P ) |
| 6 |
4
|
rneqi |
|- ran X = ran ( F |` P ) |
| 7 |
6
|
eqcomi |
|- ran ( F |` P ) = ran X |
| 8 |
7
|
a1i |
|- ( ph -> ran ( F |` P ) = ran X ) |
| 9 |
5 8
|
eqtr2id |
|- ( ph -> ran X = ( F " P ) ) |
| 10 |
1 2 3
|
fcoreslem1 |
|- ( ph -> P = ( `' F " E ) ) |
| 11 |
10
|
imaeq2d |
|- ( ph -> ( F " P ) = ( F " ( `' F " E ) ) ) |
| 12 |
1
|
ffund |
|- ( ph -> Fun F ) |
| 13 |
|
funimacnv |
|- ( Fun F -> ( F " ( `' F " E ) ) = ( E i^i ran F ) ) |
| 14 |
12 13
|
syl |
|- ( ph -> ( F " ( `' F " E ) ) = ( E i^i ran F ) ) |
| 15 |
|
inss1 |
|- ( ran F i^i C ) C_ ran F |
| 16 |
2 15
|
eqsstri |
|- E C_ ran F |
| 17 |
16
|
a1i |
|- ( ph -> E C_ ran F ) |
| 18 |
|
dfss2 |
|- ( E C_ ran F <-> ( E i^i ran F ) = E ) |
| 19 |
17 18
|
sylib |
|- ( ph -> ( E i^i ran F ) = E ) |
| 20 |
14 19
|
eqtrd |
|- ( ph -> ( F " ( `' F " E ) ) = E ) |
| 21 |
9 11 20
|
3eqtrd |
|- ( ph -> ran X = E ) |