Theorem fcoresfo

Description: If a composition is surjective, then the restriction of its first component to the minimum domain is surjective. (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 )
	fcoresfo.s	|- ( ph -> ( G o. F ) : P -onto-> D )
Assertion	fcoresfo	|- ( ph -> Y : E -onto-> D )

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		fcoresfo.s	|- ( ph -> ( G o. F ) : P -onto-> D )
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	5 10	fssresd	|- ( ph -> ( G |` E ) : E --> D )
12	6	feq1i	|- ( Y : E --> D <-> ( G |` E ) : E --> D )
13	11 12	sylibr	|- ( ph -> Y : E --> D )
14	1 2 3 4	fcoreslem3	|- ( ph -> X : P -onto-> E )
15		fof	|- ( X : P -onto-> E -> X : P --> E )
16	14 15	syl	|- ( ph -> X : P --> E )
17	1 2 3 4 5 6	fcores	|- ( ph -> ( G o. F ) = ( Y o. X ) )
18	17	eqcomd	|- ( ph -> ( Y o. X ) = ( G o. F ) )
19		foeq1	|- ( ( Y o. X ) = ( G o. F ) -> ( ( Y o. X ) : P -onto-> D <-> ( G o. F ) : P -onto-> D ) )
20	18 19	syl	|- ( ph -> ( ( Y o. X ) : P -onto-> D <-> ( G o. F ) : P -onto-> D ) )
21	7 20	mpbird	|- ( ph -> ( Y o. X ) : P -onto-> D )
22		foco2	|- ( ( Y : E --> D /\ X : P --> E /\ ( Y o. X ) : P -onto-> D ) -> Y : E -onto-> D )
23	13 16 21 22	syl3anc	|- ( ph -> Y : E -onto-> D )