Theorem fowdom

Description: An onto function implies weak dominance. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Assertion	fowdom	|- ( ( F e. V /\ F : Y -onto-> X ) -> X ~<_* Y )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( F e. V -> F e. _V )
2		foeq1	|- ( z = F -> ( z : Y -onto-> X <-> F : Y -onto-> X ) )
3	2	spcegv	|- ( F e. _V -> ( F : Y -onto-> X -> E. z z : Y -onto-> X ) )
4	3	imp	|- ( ( F e. _V /\ F : Y -onto-> X ) -> E. z z : Y -onto-> X )
5	4	olcd	|- ( ( F e. _V /\ F : Y -onto-> X ) -> ( X = (/) \/ E. z z : Y -onto-> X ) )
6		fof	|- ( F : Y -onto-> X -> F : Y --> X )
7		dmfex	|- ( ( F e. _V /\ F : Y --> X ) -> Y e. _V )
8	6 7	sylan2	|- ( ( F e. _V /\ F : Y -onto-> X ) -> Y e. _V )
9		brwdom	|- ( Y e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
10	8 9	syl	|- ( ( F e. _V /\ F : Y -onto-> X ) -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
11	5 10	mpbird	|- ( ( F e. _V /\ F : Y -onto-> X ) -> X ~<_* Y )
12	1 11	sylan	|- ( ( F e. V /\ F : Y -onto-> X ) -> X ~<_* Y )