Metamath Proof Explorer


Definition df-wdom

Description: A set isweakly 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 ) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 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)

Ref Expression
Assertion df-wdom * = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦onto𝑥 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwdom *
1 vx 𝑥
2 vy 𝑦
3 1 cv 𝑥
4 c0
5 3 4 wceq 𝑥 = ∅
6 vz 𝑧
7 6 cv 𝑧
8 2 cv 𝑦
9 8 3 7 wfo 𝑧 : 𝑦onto𝑥
10 9 6 wex 𝑧 𝑧 : 𝑦onto𝑥
11 5 10 wo ( 𝑥 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦onto𝑥 )
12 11 1 2 copab { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦onto𝑥 ) }
13 0 12 wceq * = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦onto𝑥 ) }