Theorem fcoresf1b

Description: A composition is injective iff the restrictions of its components to the minimum domains are injective. (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	fcoresf1b	|- ( ph -> ( ( G o. F ) : P -1-1-> D <-> ( X : P -1-1-> E /\ Y : E -1-1-> 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 -1-1-> D ) -> F : A --> B )
8	5	adantr	|- ( ( ph /\ ( G o. F ) : P -1-1-> D ) -> G : C --> D )
9		simpr	|- ( ( ph /\ ( G o. F ) : P -1-1-> D ) -> ( G o. F ) : P -1-1-> D )
10	7 2 3 4 8 6 9	fcoresf1	|- ( ( ph /\ ( G o. F ) : P -1-1-> D ) -> ( X : P -1-1-> E /\ Y : E -1-1-> D ) )
11	10	ex	|- ( ph -> ( ( G o. F ) : P -1-1-> D -> ( X : P -1-1-> E /\ Y : E -1-1-> D ) ) )
12		f1co	|- ( ( Y : E -1-1-> D /\ X : P -1-1-> E ) -> ( Y o. X ) : P -1-1-> D )
13	12	ancoms	|- ( ( X : P -1-1-> E /\ Y : E -1-1-> D ) -> ( Y o. X ) : P -1-1-> D )
14	1 2 3 4 5 6	fcores	|- ( ph -> ( G o. F ) = ( Y o. X ) )
15		f1eq1	|- ( ( G o. F ) = ( Y o. X ) -> ( ( G o. F ) : P -1-1-> D <-> ( Y o. X ) : P -1-1-> D ) )
16	14 15	syl	|- ( ph -> ( ( G o. F ) : P -1-1-> D <-> ( Y o. X ) : P -1-1-> D ) )
17	13 16	syl5ibr	|- ( ph -> ( ( X : P -1-1-> E /\ Y : E -1-1-> D ) -> ( G o. F ) : P -1-1-> D ) )
18	11 17	impbid	|- ( ph -> ( ( G o. F ) : P -1-1-> D <-> ( X : P -1-1-> E /\ Y : E -1-1-> D ) ) )