Metamath Proof Explorer


Theorem fcoresf1ob

Description: A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is 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 fcoresf1ob
|- ( ph -> ( ( G o. F ) : P -1-1-onto-> D <-> ( X : P -1-1-> E /\ Y : E -1-1-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 2 3 4 5 6 fcoresf1b
 |-  ( ph -> ( ( G o. F ) : P -1-1-> D <-> ( X : P -1-1-> E /\ Y : E -1-1-> D ) ) )
8 1 2 3 4 5 6 fcoresfob
 |-  ( ph -> ( ( G o. F ) : P -onto-> D <-> Y : E -onto-> D ) )
9 7 8 anbi12d
 |-  ( ph -> ( ( ( G o. F ) : P -1-1-> D /\ ( G o. F ) : P -onto-> D ) <-> ( ( X : P -1-1-> E /\ Y : E -1-1-> D ) /\ Y : E -onto-> D ) ) )
10 anass
 |-  ( ( ( X : P -1-1-> E /\ Y : E -1-1-> D ) /\ Y : E -onto-> D ) <-> ( X : P -1-1-> E /\ ( Y : E -1-1-> D /\ Y : E -onto-> D ) ) )
11 9 10 bitrdi
 |-  ( ph -> ( ( ( G o. F ) : P -1-1-> D /\ ( G o. F ) : P -onto-> D ) <-> ( X : P -1-1-> E /\ ( Y : E -1-1-> D /\ Y : E -onto-> D ) ) ) )
12 df-f1o
 |-  ( ( G o. F ) : P -1-1-onto-> D <-> ( ( G o. F ) : P -1-1-> D /\ ( G o. F ) : P -onto-> D ) )
13 df-f1o
 |-  ( Y : E -1-1-onto-> D <-> ( Y : E -1-1-> D /\ Y : E -onto-> D ) )
14 13 anbi2i
 |-  ( ( X : P -1-1-> E /\ Y : E -1-1-onto-> D ) <-> ( X : P -1-1-> E /\ ( Y : E -1-1-> D /\ Y : E -onto-> D ) ) )
15 11 12 14 3bitr4g
 |-  ( ph -> ( ( G o. F ) : P -1-1-onto-> D <-> ( X : P -1-1-> E /\ Y : E -1-1-onto-> D ) ) )