Description: The existence of omega (the class of natural numbers). Axiom 7 of TakeutiZaring p. 43. This theorem is proved assuming the Axiom of Infinity and in fact is equivalent to it, as shown by the reverse derivation inf0 .
A finitist (someone who doesn't believe in infinity) could, without contradiction, replace the Axiom of Infinity by its denial -.om e. V ; this would lead to _om = On by omon and Fin = _V (the universe of all sets) by fineqv . The finitist could still develop natural number, integer, and rational number arithmetic but would be denied the real numbers (as well as much of the rest of mathematics). In deference to the finitist, much of our development is done, when possible, without invoking the Axiom of Infinity; an example is Peano's axioms peano1 through peano5 (which many textbooks prove more easily assuming Infinity). (Contributed by NM, 6-Aug-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | omex | ⊢ ω ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zfinf2 | ⊢ ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) | |
| 2 | ax-1 | ⊢ ( ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ ω → ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) ) | |
| 3 | 2 | ralimi2 | ⊢ ( ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 → ∀ 𝑦 ∈ ω ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) |
| 4 | peano5 | ⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ ω ( 𝑦 ∈ 𝑥 → suc 𝑦 ∈ 𝑥 ) ) → ω ⊆ 𝑥 ) | |
| 5 | 3 4 | sylan2 | ⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) → ω ⊆ 𝑥 ) |
| 6 | 5 | eximi | ⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ) → ∃ 𝑥 ω ⊆ 𝑥 ) |
| 7 | vex | ⊢ 𝑥 ∈ V | |
| 8 | 7 | ssex | ⊢ ( ω ⊆ 𝑥 → ω ∈ V ) |
| 9 | 8 | exlimiv | ⊢ ( ∃ 𝑥 ω ⊆ 𝑥 → ω ∈ V ) |
| 10 | 1 6 9 | mp2b | ⊢ ω ∈ V |