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

Definition df-iom 4314
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 4105. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers with analogous properties and operations, but they will be different sets. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4315 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 4313 . 2 class ω
2 c0 3224 . . . . . 6 class
3 vx . . . . . . 7 setvar 𝑥
43cv 1242 . . . . . 6 class 𝑥
52, 4wcel 1393 . . . . 5 wff ∅ ∈ 𝑥
6 vy . . . . . . . . 9 setvar 𝑦
76cv 1242 . . . . . . . 8 class 𝑦
87csuc 4102 . . . . . . 7 class suc 𝑦
98, 4wcel 1393 . . . . . 6 wff suc 𝑦𝑥
109, 6, 4wral 2306 . . . . 5 wff 𝑦𝑥 suc 𝑦𝑥
115, 10wa 97 . . . 4 wff (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)
1211, 3cab 2026 . . 3 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
1312cint 3615 . 2 class {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
141, 13wceq 1243 1 wff ω = {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦𝑥 suc 𝑦𝑥)}
Colors of variables: wff set class
This definition is referenced by:  dfom3  4315
  Copyright terms: Public domain W3C validator