Theorem fcoreslem4

Description: Lemma 4 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 )
	fcores.x	|- X = ( F |` P )
	fcores.g	|- ( ph -> G : C --> D )
	fcores.y	|- Y = ( G |` E )
Assertion	fcoreslem4	|- ( ph -> ( Y o. X ) Fn P )

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	5	ffnd	|- ( ph -> G Fn C )
8	2	a1i	|- ( ph -> E = ( ran F i^i C ) )
9		inss2	|- ( ran F i^i C ) C_ C
10	8 9	eqsstrdi	|- ( ph -> E C_ C )
11	7 10	fnssresd	|- ( ph -> ( G |` E ) Fn E )
12	6	fneq1i	|- ( Y Fn E <-> ( G |` E ) Fn E )
13	11 12	sylibr	|- ( ph -> Y Fn E )
14	1 2 3 4	fcoreslem3	|- ( ph -> X : P -onto-> E )
15		fofn	|- ( X : P -onto-> E -> X Fn P )
16	14 15	syl	|- ( ph -> X Fn P )
17	1 2 3 4	fcoreslem2	|- ( ph -> ran X = E )
18		eqimss	|- ( ran X = E -> ran X C_ E )
19	17 18	syl	|- ( ph -> ran X C_ E )
20		fnco	|- ( ( Y Fn E /\ X Fn P /\ ran X C_ E ) -> ( Y o. X ) Fn P )
21	13 16 19 20	syl3anc	|- ( ph -> ( Y o. X ) Fn P )