Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-om | Structured version Visualization version GIF version |
Description: Define the class of
natural numbers, which are all ordinal numbers that
are less than every limit ordinal, i.e. all finite ordinals. Our
definition is a variant of the Definition of N of [BellMachover] p. 471.
See dfom2 7067 for an alternate definition. Later, when we
assume the
Axiom of Infinity, we show ω is a set in
omex 8540, and ω can
then be defined per dfom3 8544 (the smallest inductive set) and dfom4 8546.
Note: the natural numbers ω are a subset of the ordinal numbers df-on 5727. They are completely different from the natural numbers ℕ (df-nn 11021) that are a subset of the complex numbers defined much later in our development, although the two sets have analogous properties and operations defined on them. (Contributed by NM, 15-May-1994.) |
Ref | Expression |
---|---|
df-om | ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com 7065 | . 2 class ω | |
2 | vy | . . . . . . 7 setvar 𝑦 | |
3 | 2 | cv 1482 | . . . . . 6 class 𝑦 |
4 | 3 | wlim 5724 | . . . . 5 wff Lim 𝑦 |
5 | vx | . . . . . 6 setvar 𝑥 | |
6 | 5, 2 | wel 1991 | . . . . 5 wff 𝑥 ∈ 𝑦 |
7 | 4, 6 | wi 4 | . . . 4 wff (Lim 𝑦 → 𝑥 ∈ 𝑦) |
8 | 7, 2 | wal 1481 | . . 3 wff ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦) |
9 | con0 5723 | . . 3 class On | |
10 | 8, 5, 9 | crab 2916 | . 2 class {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} |
11 | 1, 10 | wceq 1483 | 1 wff ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfom2 7067 elom 7068 |
Copyright terms: Public domain | W3C validator |