Theorem fcoresf1lem

Description: Lemma for fcoresf1 . (Contributed by AV, 18-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 )
	fcores.g	|- ( ph -> G : C --> D )
	fcores.y	|- Y = ( G |` E )
Assertion	fcoresf1lem	|- ( ( ph /\ Z e. P ) -> ( ( G o. F ) ` Z ) = ( Y ` ( X ` Z ) ) )

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		fcores.g	|- ( ph -> G : C --> D )
6		fcores.y	|- Y = ( G |` E )
7	1 2 3 4 5 6	fcores	|- ( ph -> ( G o. F ) = ( Y o. X ) )
8	7	fveq1d	|- ( ph -> ( ( G o. F ) ` Z ) = ( ( Y o. X ) ` Z ) )
9	8	adantr	|- ( ( ph /\ Z e. P ) -> ( ( G o. F ) ` Z ) = ( ( Y o. X ) ` Z ) )
10	1 2 3 4	fcoreslem3	|- ( ph -> X : P -onto-> E )
11		fof	|- ( X : P -onto-> E -> X : P --> E )
12	10 11	syl	|- ( ph -> X : P --> E )
13	12	adantr	|- ( ( ph /\ Z e. P ) -> X : P --> E )
14		simpr	|- ( ( ph /\ Z e. P ) -> Z e. P )
15	13 14	fvco3d	|- ( ( ph /\ Z e. P ) -> ( ( Y o. X ) ` Z ) = ( Y ` ( X ` Z ) ) )
16	9 15	eqtrd	|- ( ( ph /\ Z e. P ) -> ( ( G o. F ) ` Z ) = ( Y ` ( X ` Z ) ) )