Metamath Proof Explorer

Theorem brwdomi

Description: Property of weak dominance, forward direction only. (Contributed by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion brwdomi 
|- ( X ~<_* Y -> ( X = (/) \/ E. z z : Y -onto-> X ) )

Proof

Step Hyp Ref Expression
1 relwdom 
 |-  Rel ~<_*
2 1 brrelex2i 
 |-  ( X ~<_* Y -> Y e. _V )
3 brwdom 
 |-  ( Y e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
4 2 3 syl 
 |-  ( X ~<_* Y -> ( X ~<_* Y <-> ( X = (/) \/ E. z z : Y -onto-> X ) ) )
5 4 ibi 
 |-  ( X ~<_* Y -> ( X = (/) \/ E. z z : Y -onto-> X ) )