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

Metamath Proof Explorer

Theorem fcoresfo

Description: If a composition is surjective, then the restriction of its first component to the minimum domain is surjective. (Contributed by AV, 17-Sep-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 )
fcoresfo.s 
|- ( ph -> ( G o. F ) : P -onto-> D )
Assertion fcoresfo 
|- ( ph -> 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 fcoresfo.s 
 |-  ( ph -> ( G o. F ) : P -onto-> D )
8 2 a1i 
 |-  ( ph -> E = ( ran F i^i C ) )
9 inss2 
 |-  ( ran F i^i C ) C_ C
10 8 9 eqsstrdi 
 |-  ( ph -> E C_ C )
11 5 10 fssresd 
 |-  ( ph -> ( G |` E ) : E --> D )
12 6 feq1i 
 |-  ( Y : E --> D <-> ( G |` E ) : E --> D )
13 11 12 sylibr 
 |-  ( ph -> Y : E --> D )
14 1 2 3 4 fcoreslem3 
 |-  ( ph -> X : P -onto-> E )
15 fof 
 |-  ( X : P -onto-> E -> X : P --> E )
16 14 15 syl 
 |-  ( ph -> X : P --> E )
17 1 2 3 4 5 6 fcores 
 |-  ( ph -> ( G o. F ) = ( Y o. X ) )
18 17 eqcomd 
 |-  ( ph -> ( Y o. X ) = ( G o. F ) )
19 foeq1 
 |-  ( ( Y o. X ) = ( G o. F ) -> ( ( Y o. X ) : P -onto-> D <-> ( G o. F ) : P -onto-> D ) )
20 18 19 syl 
 |-  ( ph -> ( ( Y o. X ) : P -onto-> D <-> ( G o. F ) : P -onto-> D ) )
21 7 20 mpbird 
 |-  ( ph -> ( Y o. X ) : P -onto-> D )
22 foco2 
 |-  ( ( Y : E --> D /\ X : P --> E /\ ( Y o. X ) : P -onto-> D ) -> Y : E -onto-> D )
23 13 16 21 22 syl3anc 
 |-  ( ph -> Y : E -onto-> D )