Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfwdom  Unicode version 
Description: A set is weakly dominated by a "larger" set iff the "larger" set can be mapped onto the "smaller" set or the smaller set is empty; equivalently if the smaller set can be placed into bijection with some partition of the larger set. When choice is assumed (as fodom 8358), this concides with the 11 defition dfdom 7070; however, it is not known whether this is a choiceequivalent or a strictly weaker form. Some discussion of this question can be found at http://boolesrings.org/asafk/2014/onthepartitionprinciple/. (Contributed by Stefan O'Rear, 11Feb2015.) 
Ref  Expression 

dfwdom  ^{*} 
Step  Hyp  Ref  Expression 

1  cwdom 7481  . 2 ^{*}  
2  vx  . . . . . 6  
3  2  cv 1648  . . . . 5 
4  c0 3588  . . . . 5  
5  3, 4  wceq 1649  . . . 4 
6  vy  . . . . . . 7  
7  6  cv 1648  . . . . . 6 
8  vz  . . . . . . 7  
9  8  cv 1648  . . . . . 6 
10  7, 3, 9  wfo 5411  . . . . 5 
11  10, 8  wex 1547  . . . 4 
12  5, 11  wo 358  . . 3 
13  12, 2, 6  copab 4225  . 2 
14  1, 13  wceq 1649  1 ^{*} 
Colors of variables: wff set class 
This definition is referenced by: relwdom 7490 brwdom 7491 
Copyright terms: Public domain  W3C validator 