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

Metamath Proof Explorer

Theorem wdompwdom

Description: Weak dominance strengthens to usual dominance on the power sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

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

Proof

Step Hyp Ref Expression
1 relwdom 
 |-  Rel ~<_*
2 1 brrelex2i 
 |-  ( X ~<_* Y -> Y e. _V )
3 2 pwexd 
 |-  ( X ~<_* Y -> ~P Y e. _V )
4 0ss 
 |-  (/) C_ Y
5 4 sspwi 
 |-  ~P (/) C_ ~P Y
6 ssdomg 
 |-  ( ~P Y e. _V -> ( ~P (/) C_ ~P Y -> ~P (/) ~<_ ~P Y ) )
7 3 5 6 mpisyl 
 |-  ( X ~<_* Y -> ~P (/) ~<_ ~P Y )
8 pweq 
 |-  ( X = (/) -> ~P X = ~P (/) )
9 8 breq1d 
 |-  ( X = (/) -> ( ~P X ~<_ ~P Y <-> ~P (/) ~<_ ~P Y ) )
10 7 9 imbitrrid 
 |-  ( X = (/) -> ( X ~<_* Y -> ~P X ~<_ ~P Y ) )
11 brwdomn0 
 |-  ( X =/= (/) -> ( X ~<_* Y <-> E. z z : Y -onto-> X ) )
12 vex 
 |-  z e. _V
13 fopwdom 
 |-  ( ( z e. _V /\ z : Y -onto-> X ) -> ~P X ~<_ ~P Y )
14 12 13 mpan 
 |-  ( z : Y -onto-> X -> ~P X ~<_ ~P Y )
15 14 exlimiv 
 |-  ( E. z z : Y -onto-> X -> ~P X ~<_ ~P Y )
16 11 15 biimtrdi 
 |-  ( X =/= (/) -> ( X ~<_* Y -> ~P X ~<_ ~P Y ) )
17 10 16 pm2.61ine 
 |-  ( X ~<_* Y -> ~P X ~<_ ~P Y )