Theorem fcoresfob

Description: A composition is surjective iff the restriction of its first component to the minimum domain is surjective. (Contributed by GL and AV, 7-Oct-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	fcoresfob	|- ( ph -> ( ( G o. F ) : P -onto-> D <-> 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	1	adantr	|- ( ( ph /\ ( G o. F ) : P -onto-> D ) -> F : A --> B )
8	5	adantr	|- ( ( ph /\ ( G o. F ) : P -onto-> D ) -> G : C --> D )
9		simpr	|- ( ( ph /\ ( G o. F ) : P -onto-> D ) -> ( G o. F ) : P -onto-> D )
10	7 2 3 4 8 6 9	fcoresfo	|- ( ( ph /\ ( G o. F ) : P -onto-> D ) -> Y : E -onto-> D )
11	1 2 3 4	fcoreslem3	|- ( ph -> X : P -onto-> E )
12	11	anim1ci	|- ( ( ph /\ Y : E -onto-> D ) -> ( Y : E -onto-> D /\ X : P -onto-> E ) )
13		foco	|- ( ( Y : E -onto-> D /\ X : P -onto-> E ) -> ( Y o. X ) : P -onto-> D )
14	12 13	syl	|- ( ( ph /\ Y : E -onto-> D ) -> ( Y o. X ) : P -onto-> D )
15	1 2 3 4 5 6	fcores	|- ( ph -> ( G o. F ) = ( Y o. X ) )
16	15	adantr	|- ( ( ph /\ Y : E -onto-> D ) -> ( G o. F ) = ( Y o. X ) )
17		foeq1	|- ( ( G o. F ) = ( Y o. X ) -> ( ( G o. F ) : P -onto-> D <-> ( Y o. X ) : P -onto-> D ) )
18	16 17	syl	|- ( ( ph /\ Y : E -onto-> D ) -> ( ( G o. F ) : P -onto-> D <-> ( Y o. X ) : P -onto-> D ) )
19	14 18	mpbird	|- ( ( ph /\ Y : E -onto-> D ) -> ( G o. F ) : P -onto-> D )
20	10 19	impbida	|- ( ph -> ( ( G o. F ) : P -onto-> D <-> Y : E -onto-> D ) )