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

Metamath Proof Explorer

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