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 )