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

Metamath Proof Explorer

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 )