Theorem fcoreslem1

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 ) )

Proof

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 ) )