![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-iom | GIF version |
Description: Define the class of
natural numbers as the smallest inductive set, which
is valid provided we assume the Axiom of Infinity. Definition 6.3 of
[Eisenberg] p. 82.
Note: the natural numbers ω are a subset of the ordinal numbers df-on 4382. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-inn 8937) with analogous properties and operations, but they will be different sets. We are unable to use the terms finite ordinal and natural number interchangeably, as shown at exmidonfin 7210. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4605 instead for naming consistency with set.mm. (New usage is discouraged.) |
Ref | Expression |
---|---|
df-iom | ⊢ ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com 4603 | . 2 class ω | |
2 | c0 3436 | . . . . . 6 class ∅ | |
3 | vx | . . . . . . 7 setvar 𝑥 | |
4 | 3 | cv 1362 | . . . . . 6 class 𝑥 |
5 | 2, 4 | wcel 2159 | . . . . 5 wff ∅ ∈ 𝑥 |
6 | vy | . . . . . . . . 9 setvar 𝑦 | |
7 | 6 | cv 1362 | . . . . . . . 8 class 𝑦 |
8 | 7 | csuc 4379 | . . . . . . 7 class suc 𝑦 |
9 | 8, 4 | wcel 2159 | . . . . . 6 wff suc 𝑦 ∈ 𝑥 |
10 | 9, 6, 4 | wral 2467 | . . . . 5 wff ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 |
11 | 5, 10 | wa 104 | . . . 4 wff (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) |
12 | 11, 3 | cab 2174 | . . 3 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
13 | 12 | cint 3858 | . 2 class ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
14 | 1, 13 | wceq 1363 | 1 wff ω = ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
Colors of variables: wff set class |
This definition is referenced by: dfom3 4605 |
Copyright terms: Public domain | W3C validator |