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

Metamath Proof Explorer

Theorem domwdom

Description: Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion domwdom 
|- ( X ~<_ Y -> X ~<_* Y )

Proof

Step Hyp Ref Expression
1 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
2 1 adantl 
 |-  ( ( X ~<_ Y /\ -. X = (/) ) -> X =/= (/) )
3 reldom 
 |-  Rel ~<_
4 3 brrelex1i 
 |-  ( X ~<_ Y -> X e. _V )
5 0sdomg 
 |-  ( X e. _V -> ( (/) ~< X <-> X =/= (/) ) )
6 4 5 syl 
 |-  ( X ~<_ Y -> ( (/) ~< X <-> X =/= (/) ) )
7 6 adantr 
 |-  ( ( X ~<_ Y /\ -. X = (/) ) -> ( (/) ~< X <-> X =/= (/) ) )
8 2 7 mpbird 
 |-  ( ( X ~<_ Y /\ -. X = (/) ) -> (/) ~< X )
9 simpl 
 |-  ( ( X ~<_ Y /\ -. X = (/) ) -> X ~<_ Y )
10 fodomr 
 |-  ( ( (/) ~< X /\ X ~<_ Y ) -> E. y y : Y -onto-> X )
11 8 9 10 syl2anc 
 |-  ( ( X ~<_ Y /\ -. X = (/) ) -> E. y y : Y -onto-> X )
12 11 ex 
 |-  ( X ~<_ Y -> ( -. X = (/) -> E. y y : Y -onto-> X ) )
13 12 orrd 
 |-  ( X ~<_ Y -> ( X = (/) \/ E. y y : Y -onto-> X ) )
14 3 brrelex2i 
 |-  ( X ~<_ Y -> Y e. _V )
15 brwdom 
 |-  ( Y e. _V -> ( X ~<_* Y <-> ( X = (/) \/ E. y y : Y -onto-> X ) ) )
16 14 15 syl 
 |-  ( X ~<_ Y -> ( X ~<_* Y <-> ( X = (/) \/ E. y y : Y -onto-> X ) ) )
17 13 16 mpbird 
 |-  ( X ~<_ Y -> X ~<_* Y )