MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wdompwdom Structured version   Unicode version

Theorem wdompwdom 7937
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.)
Assertion
Ref Expression
wdompwdom  |-  ( X  ~<_*  Y  ->  ~P X  ~<_  ~P Y )

Proof of Theorem wdompwdom
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 relwdom 7925 . . . . . 6  |-  Rel  ~<_*
21brrelex2i 4968 . . . . 5  |-  ( X  ~<_*  Y  ->  Y  e.  _V )
3 pwexg 4562 . . . . 5  |-  ( Y  e.  _V  ->  ~P Y  e.  _V )
42, 3syl 16 . . . 4  |-  ( X  ~<_*  Y  ->  ~P Y  e. 
_V )
5 0ss 3754 . . . . 5  |-  (/)  C_  Y
6 sspwb 4624 . . . . 5  |-  ( (/)  C_  Y  <->  ~P (/)  C_  ~P Y
)
75, 6mpbi 208 . . . 4  |-  ~P (/)  C_  ~P Y
8 ssdomg 7498 . . . 4  |-  ( ~P Y  e.  _V  ->  ( ~P (/)  C_  ~P Y  ->  ~P (/)  ~<_  ~P Y
) )
94, 7, 8mpisyl 18 . . 3  |-  ( X  ~<_*  Y  ->  ~P (/)  ~<_  ~P Y
)
10 pweq 3943 . . . 4  |-  ( X  =  (/)  ->  ~P X  =  ~P (/) )
1110breq1d 4390 . . 3  |-  ( X  =  (/)  ->  ( ~P X  ~<_  ~P Y  <->  ~P (/)  ~<_  ~P Y
) )
129, 11syl5ibr 221 . 2  |-  ( X  =  (/)  ->  ( X  ~<_*  Y  ->  ~P X  ~<_  ~P Y ) )
13 brwdomn0 7928 . . 3  |-  ( X  =/=  (/)  ->  ( X  ~<_*  Y  <->  E. z  z : Y -onto-> X ) )
14 vex 3050 . . . . 5  |-  z  e. 
_V
15 fopwdom 7562 . . . . 5  |-  ( ( z  e.  _V  /\  z : Y -onto-> X )  ->  ~P X  ~<_  ~P Y )
1614, 15mpan 668 . . . 4  |-  ( z : Y -onto-> X  ->  ~P X  ~<_  ~P Y
)
1716exlimiv 1737 . . 3  |-  ( E. z  z : Y -onto-> X  ->  ~P X  ~<_  ~P Y )
1813, 17syl6bi 228 . 2  |-  ( X  =/=  (/)  ->  ( X  ~<_*  Y  ->  ~P X  ~<_  ~P Y ) )
1912, 18pm2.61ine 2705 1  |-  ( X  ~<_*  Y  ->  ~P X  ~<_  ~P Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399   E.wex 1627    e. wcel 1836    =/= wne 2587   _Vcvv 3047    C_ wss 3402   (/)c0 3724   ~Pcpw 3940   class class class wbr 4380   -onto->wfo 5507    ~<_ cdom 7451    ~<_* cwdom 7916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-dom 7455  df-wdom 7918
This theorem is referenced by:  isfin32i  8676  hsmexlem1  8737  hsmexlem3  8739  gchhar  8986
  Copyright terms: Public domain W3C validator