![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-wdom | Structured version Visualization version GIF version |
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 8943) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10520 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 |
---|---|
df-wdom | ⊢ ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cwdom 9561 | . 2 class ≼* | |
2 | vx | . . . . . 6 setvar 𝑥 | |
3 | 2 | cv 1538 | . . . . 5 class 𝑥 |
4 | c0 4321 | . . . . 5 class ∅ | |
5 | 3, 4 | wceq 1539 | . . . 4 wff 𝑥 = ∅ |
6 | vy | . . . . . . 7 setvar 𝑦 | |
7 | 6 | cv 1538 | . . . . . 6 class 𝑦 |
8 | vz | . . . . . . 7 setvar 𝑧 | |
9 | 8 | cv 1538 | . . . . . 6 class 𝑧 |
10 | 7, 3, 9 | wfo 6540 | . . . . 5 wff 𝑧:𝑦–onto→𝑥 |
11 | 10, 8 | wex 1779 | . . . 4 wff ∃𝑧 𝑧:𝑦–onto→𝑥 |
12 | 5, 11 | wo 843 | . . 3 wff (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥) |
13 | 12, 2, 6 | copab 5209 | . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} |
14 | 1, 13 | wceq 1539 | 1 wff ≼* = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦–onto→𝑥)} |
Colors of variables: wff setvar class |
This definition is referenced by: relwdom 9563 brwdom 9564 |
Copyright terms: Public domain | W3C validator |