Theorem dffo5

Description: Alternate definition of an onto mapping. (Contributed by NM, 20-Mar-2007)

	Ref	Expression
Assertion	dffo5	|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x x F y ) )

Proof

Step	Hyp	Ref	Expression
1		dffo4	|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
2		rexex	|- ( E. x e. A x F y -> E. x x F y )
3	2	ralimi	|- ( A. y e. B E. x e. A x F y -> A. y e. B E. x x F y )
4	3	anim2i	|- ( ( F : A --> B /\ A. y e. B E. x e. A x F y ) -> ( F : A --> B /\ A. y e. B E. x x F y ) )
5		ffn	|- ( F : A --> B -> F Fn A )
6		fnbr	|- ( ( F Fn A /\ x F y ) -> x e. A )
7	6	ex	|- ( F Fn A -> ( x F y -> x e. A ) )
8	5 7	syl	|- ( F : A --> B -> ( x F y -> x e. A ) )
9	8	ancrd	|- ( F : A --> B -> ( x F y -> ( x e. A /\ x F y ) ) )
10	9	eximdv	|- ( F : A --> B -> ( E. x x F y -> E. x ( x e. A /\ x F y ) ) )
11		df-rex	|- ( E. x e. A x F y <-> E. x ( x e. A /\ x F y ) )
12	10 11	syl6ibr	|- ( F : A --> B -> ( E. x x F y -> E. x e. A x F y ) )
13	12	ralimdv	|- ( F : A --> B -> ( A. y e. B E. x x F y -> A. y e. B E. x e. A x F y ) )
14	13	imdistani	|- ( ( F : A --> B /\ A. y e. B E. x x F y ) -> ( F : A --> B /\ A. y e. B E. x e. A x F y ) )
15	4 14	impbii	|- ( ( F : A --> B /\ A. y e. B E. x e. A x F y ) <-> ( F : A --> B /\ A. y e. B E. x x F y ) )
16	1 15	bitri	|- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x x F y ) )