ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-iom GIF version

Definition df-iom 4575
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 4353. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-inn 8879) 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 7171. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4576 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion
Ref Expression
df-iom ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-iom
StepHypRef Expression
1 com 4574 . 2 class ω
2 c0 3414 . . . . . 6 class
3 vx . . . . . . 7 setvar 𝑥
43cv 1347 . . . . . 6 class 𝑥
52, 4wcel 2141 . . . . 5 wff ∅ ∈ 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1347 . . . . . . . 8 class 𝑦
87csuc 4350 . . . . . . 7 class suc 𝑦
98, 4wcel 2141 . . . . . 6 wff suc 𝑦𝑥
109, 6, 4wral 2448 . . . . 5 wff 𝑦𝑥 suc 𝑦𝑥
115, 10wa 103 . . . 4 wff (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
1211, 3cab 2156 . . 3 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
1312cint 3831 . 2 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
141, 13wceq 1348 1 wff ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
Colors of variables: wff set class
This definition is referenced by:  dfom3  4576
  Copyright terms: Public domain W3C validator