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

Metamath Proof Explorer

Theorem foco2

Description: If a composition of two functions is surjective, then the function on the left is surjective. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion foco2 
|- ( ( F : B --> C /\ G : A --> B /\ ( F o. G ) : A -onto-> C ) -> F : B -onto-> C )

Proof

Step Hyp Ref Expression
1 foelrn 
 |-  ( ( ( F o. G ) : A -onto-> C /\ y e. C ) -> E. z e. A y = ( ( F o. G ) ` z ) )
2 ffvelcdm 
 |-  ( ( G : A --> B /\ z e. A ) -> ( G ` z ) e. B )
3 fvco3 
 |-  ( ( G : A --> B /\ z e. A ) -> ( ( F o. G ) ` z ) = ( F ` ( G ` z ) ) )
4 fveq2 
 |-  ( x = ( G ` z ) -> ( F ` x ) = ( F ` ( G ` z ) ) )
5 4 rspceeqv 
 |-  ( ( ( G ` z ) e. B /\ ( ( F o. G ) ` z ) = ( F ` ( G ` z ) ) ) -> E. x e. B ( ( F o. G ) ` z ) = ( F ` x ) )
6 2 3 5 syl2anc 
 |-  ( ( G : A --> B /\ z e. A ) -> E. x e. B ( ( F o. G ) ` z ) = ( F ` x ) )
7 eqeq1 
 |-  ( y = ( ( F o. G ) ` z ) -> ( y = ( F ` x ) <-> ( ( F o. G ) ` z ) = ( F ` x ) ) )
8 7 rexbidv 
 |-  ( y = ( ( F o. G ) ` z ) -> ( E. x e. B y = ( F ` x ) <-> E. x e. B ( ( F o. G ) ` z ) = ( F ` x ) ) )
9 6 8 syl5ibrcom 
 |-  ( ( G : A --> B /\ z e. A ) -> ( y = ( ( F o. G ) ` z ) -> E. x e. B y = ( F ` x ) ) )
10 9 rexlimdva 
 |-  ( G : A --> B -> ( E. z e. A y = ( ( F o. G ) ` z ) -> E. x e. B y = ( F ` x ) ) )
11 1 10 syl5 
 |-  ( G : A --> B -> ( ( ( F o. G ) : A -onto-> C /\ y e. C ) -> E. x e. B y = ( F ` x ) ) )
12 11 impl 
 |-  ( ( ( G : A --> B /\ ( F o. G ) : A -onto-> C ) /\ y e. C ) -> E. x e. B y = ( F ` x ) )
13 12 ralrimiva 
 |-  ( ( G : A --> B /\ ( F o. G ) : A -onto-> C ) -> A. y e. C E. x e. B y = ( F ` x ) )
14 13 anim2i 
 |-  ( ( F : B --> C /\ ( G : A --> B /\ ( F o. G ) : A -onto-> C ) ) -> ( F : B --> C /\ A. y e. C E. x e. B y = ( F ` x ) ) )
15 3anass 
 |-  ( ( F : B --> C /\ G : A --> B /\ ( F o. G ) : A -onto-> C ) <-> ( F : B --> C /\ ( G : A --> B /\ ( F o. G ) : A -onto-> C ) ) )
16 dffo3 
 |-  ( F : B -onto-> C <-> ( F : B --> C /\ A. y e. C E. x e. B y = ( F ` x ) ) )
17 14 15 16 3imtr4i 
 |-  ( ( F : B --> C /\ G : A --> B /\ ( F o. G ) : A -onto-> C ) -> F : B -onto-> C )