Theorem dffo2

Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006)

	Ref	Expression
Assertion	dffo2	|- ( F : A -onto-> B <-> ( F : A --> B /\ ran F = B ) )

Proof

Step	Hyp	Ref	Expression
1		fof	|- ( F : A -onto-> B -> F : A --> B )
2		forn	|- ( F : A -onto-> B -> ran F = B )
3	1 2	jca	|- ( F : A -onto-> B -> ( F : A --> B /\ ran F = B ) )
4		ffn	|- ( F : A --> B -> F Fn A )
5		df-fo	|- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
6	5	biimpri	|- ( ( F Fn A /\ ran F = B ) -> F : A -onto-> B )
7	4 6	sylan	|- ( ( F : A --> B /\ ran F = B ) -> F : A -onto-> B )
8	3 7	impbii	|- ( F : A -onto-> B <-> ( F : A --> B /\ ran F = B ) )