Theorem fcoreslem3

Description: Lemma 3 for fcores . (Contributed by AV, 13-Sep-2024)

	Ref	Expression
Hypotheses	fcores.f	|- ( ph -> F : A --> B )
	fcores.e	|- E = ( ran F i^i C )
	fcores.p	|- P = ( `' F " C )
	fcores.x	|- X = ( F |` P )
Assertion	fcoreslem3	|- ( ph -> X : P -onto-> 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		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 )