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	⊢ ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-wdom

Step	Hyp	Ref	Expression
1		cwdom 8462	. 2 class ≼*
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1482	. . . . 5 class 𝑥
4		c0 3915	. . . . 5 class ∅
5	3, 4	wceq 1483	. . . 4 wff 𝑥 = ∅
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1482	. . . . . 6 class 𝑦
8		vz	. . . . . . 7 setvar 𝑧
9	8	cv 1482	. . . . . 6 class 𝑧
10	7, 3, 9	wfo 5886	. . . . 5 wff 𝑧:𝑦–onto→𝑥
11	10, 8	wex 1704	. . . 4 wff ∃𝑧 𝑧:𝑦–onto→𝑥
12	5, 11	wo 383	. . 3 wff (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)
13	12, 2, 6	copab 4712	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}
14	1, 13	wceq 1483	1 wff ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}

This definition is referenced by:  relwdom  8471  brwdom  8472