This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrrid 
 |-  ( 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 ) ) )