Definition df-wdom 8733

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 9659), this coincides with the 1-1 definition df-dom 8224; 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 8731	. 2 class ≼*
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1655	. . . . 5 class 𝑥
4		c0 4144	. . . . 5 class ∅
5	3, 4	wceq 1656	. . . 4 wff 𝑥 = ∅
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1655	. . . . . 6 class 𝑦
8		vz	. . . . . . 7 setvar 𝑧
9	8	cv 1655	. . . . . 6 class 𝑧
10	7, 3, 9	wfo 6121	. . . . 5 wff 𝑧:𝑦–onto→𝑥
11	10, 8	wex 1878	. . . 4 wff ∃𝑧 𝑧:𝑦–onto→𝑥
12	5, 11	wo 878	. . 3 wff (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)
13	12, 2, 6	copab 4935	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}
14	1, 13	wceq 1656	1 wff ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}

This definition is referenced by:  relwdom  8740  brwdom  8741