Definition df-wdom 8464

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 9344), this coincides with the 1-1 definition df-dom 7957; however, it is not known whether this is a choice-equivalent or a strictly weaker form. Some discussion of this question can be found at http://boolesrings.org/asafk/2014/on-the-partition-principle/. (Contributed by Stefan O'Rear, 11-Feb-2015.)

Assertion

Ref	Expression
df-wdom	|- ~<_* = { <. x , y >. | ( x = (/) \/ E. z z : y -onto-> x ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-wdom

Step	Hyp	Ref	Expression
1		cwdom 8462	. 2 class ~<_*
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		c0 3915	. . . . 5 class (/)
5	3, 4	wceq 1483	. . . 4 wff x = (/)
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8		vz	. . . . . . 7 setvar z
9	8	cv 1482	. . . . . 6 class z
10	7, 3, 9	wfo 5886	. . . . 5 wff z : y -onto-> x
11	10, 8	wex 1704	. . . 4 wff E. z z : y -onto-> x
12	5, 11	wo 383	. . 3 wff ( x = (/) \/ E. z z : y -onto-> x )
13	12, 2, 6	copab 4712	. 2 class { <. x , y >. | ( x = (/) \/ E. z z : y -onto-> x ) }
14	1, 13	wceq 1483	1 wff ~<_* = { <. x , y >. | ( x = (/) \/ E. z z : y -onto-> x ) }

This definition is referenced by:  relwdom  8471  brwdom  8472