Metamath Proof Explorer

Theorem 0wdom

Description: Any set weakly dominates the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion 0wdom 
|- ( X e. V -> (/) ~<_* X )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 1 orci 
 |-  ( (/) = (/) \/ E. z z : X -onto-> (/) )
3 brwdom 
 |-  ( X e. V -> ( (/) ~<_* X <-> ( (/) = (/) \/ E. z z : X -onto-> (/) ) ) )
4 2 3 mpbiri 
 |-  ( X e. V -> (/) ~<_* X )