Definition df-wdom 9566

Description: A set is weakly dominated by a "larger" set if the "larger" set can be mapped onto the "smaller" set or the smaller set is empty, or equivalently, if the smaller set can be placed into bijection with some partition of the larger set. Dominance (df-dom 8983) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10608 proves that the axiom of choice implies the partition principle (over ZF). It is not known whether the partition principle is equivalent to the axiom of choice (over ZF), although it is know to imply dependent choice. (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 9565	. 2 class ≼*
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1568	. . . . 5 class 𝑥
4		c0 4277	. . . . 5 class ∅
5	3, 4	wceq 1569	. . . 4 wff 𝑥 = ∅
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1568	. . . . . 6 class 𝑦
8		vz	. . . . . . 7 setvar 𝑧
9	8	cv 1568	. . . . . 6 class 𝑧
10	7, 3, 9	wfo 6541	. . . . 5 wff 𝑧:𝑦–onto→𝑥
11	10, 8	wex 1811	. . . 4 wff ∃𝑧 𝑧:𝑦–onto→𝑥
12	5, 11	wo 861	. . 3 wff (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)
13	12, 2, 6	copab 5166	. 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}
14	1, 13	wceq 1569	1 wff ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)}

This definition is used by:  relwdom  9567  brwdom  9568