MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wdom Structured version   Visualization version   GIF version

Definition df-wdom 9095
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 8550) implies weak dominance (over ZF). The principle asserting the converse is known as the partition principle and is independent of ZF. Theorem fodom 10016 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
StepHypRef Expression
1 cwdom 9094 . 2 class *
2 vx . . . . . 6 setvar 𝑥
32cv 1541 . . . . 5 class 𝑥
4 c0 4209 . . . . 5 class
53, 4wceq 1542 . . . 4 wff 𝑥 = ∅
6 vy . . . . . . 7 setvar 𝑦
76cv 1541 . . . . . 6 class 𝑦
8 vz . . . . . . 7 setvar 𝑧
98cv 1541 . . . . . 6 class 𝑧
107, 3, 9wfo 6331 . . . . 5 wff 𝑧:𝑦onto𝑥
1110, 8wex 1786 . . . 4 wff 𝑧 𝑧:𝑦onto𝑥
125, 11wo 846 . . 3 wff (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦onto𝑥)
1312, 2, 6copab 5089 . 2 class {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦onto𝑥)}
141, 13wceq 1542 1 wff * = {⟨𝑥, 𝑦⟩ ∣ (𝑥 = ∅ ∨ ∃𝑧 𝑧:𝑦onto𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  relwdom  9096  brwdom  9097
  Copyright terms: Public domain W3C validator