Description: Lemma 1 for fcores . (Contributed by AV, 17-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fcores.f | |- ( ph -> F : A --> B ) |
|
fcores.e | |- E = ( ran F i^i C ) |
||
fcores.p | |- P = ( `' F " C ) |
||
Assertion | fcoreslem1 | |- ( ph -> P = ( `' F " E ) ) |
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 | 1 | ffund | |- ( ph -> Fun F ) |
5 | cnvimainrn | |- ( Fun F -> ( `' F " ( ran F i^i C ) ) = ( `' F " C ) ) |
|
6 | 4 5 | syl | |- ( ph -> ( `' F " ( ran F i^i C ) ) = ( `' F " C ) ) |
7 | 6 | eqcomd | |- ( ph -> ( `' F " C ) = ( `' F " ( ran F i^i C ) ) ) |
8 | 2 | imaeq2i | |- ( `' F " E ) = ( `' F " ( ran F i^i C ) ) |
9 | 7 3 8 | 3eqtr4g | |- ( ph -> P = ( `' F " E ) ) |