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

Metamath Proof Explorer

Theorem fcofo

Description: An application is surjective if a section exists. Proposition 8 of BourbakiEns p. E.II.18. (Contributed by FL, 17-Nov-2011) (Proof shortened by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion fcofo 
|- ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) -> F : A -onto-> B )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) -> F : A --> B )
2 ffvelcdm 
 |-  ( ( S : B --> A /\ y e. B ) -> ( S ` y ) e. A )
3 2 3ad2antl2 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> ( S ` y ) e. A )
4 simpl3 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> ( F o. S ) = ( _I |` B ) )
5 4 fveq1d 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> ( ( F o. S ) ` y ) = ( ( _I |` B ) ` y ) )
6 fvco3 
 |-  ( ( S : B --> A /\ y e. B ) -> ( ( F o. S ) ` y ) = ( F ` ( S ` y ) ) )
7 6 3ad2antl2 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> ( ( F o. S ) ` y ) = ( F ` ( S ` y ) ) )
8 fvresi 
 |-  ( y e. B -> ( ( _I |` B ) ` y ) = y )
9 8 adantl 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> ( ( _I |` B ) ` y ) = y )
10 5 7 9 3eqtr3rd 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> y = ( F ` ( S ` y ) ) )
11 fveq2 
 |-  ( x = ( S ` y ) -> ( F ` x ) = ( F ` ( S ` y ) ) )
12 11 rspceeqv 
 |-  ( ( ( S ` y ) e. A /\ y = ( F ` ( S ` y ) ) ) -> E. x e. A y = ( F ` x ) )
13 3 10 12 syl2anc 
 |-  ( ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) /\ y e. B ) -> E. x e. A y = ( F ` x ) )
14 13 ralrimiva 
 |-  ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) -> A. y e. B E. x e. A y = ( F ` x ) )
15 dffo3 
 |-  ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
16 1 14 15 sylanbrc 
 |-  ( ( F : A --> B /\ S : B --> A /\ ( F o. S ) = ( _I |` B ) ) -> F : A -onto-> B )