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

Definition df-iom 4587
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  om are a subset of the ordinal numbers df-on 4365. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-inn 8909) 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 7187. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4588 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion
Ref Expression
df-iom  |-  om  =  |^| { x  |  (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x ) }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-iom
StepHypRef Expression
1 com 4586 . 2  class  om
2 c0 3422 . . . . . 6  class  (/)
3 vx . . . . . . 7  setvar  x
43cv 1352 . . . . . 6  class  x
52, 4wcel 2148 . . . . 5  wff  (/)  e.  x
6 vy . . . . . . . . 9  setvar  y
76cv 1352 . . . . . . . 8  class  y
87csuc 4362 . . . . . . 7  class  suc  y
98, 4wcel 2148 . . . . . 6  wff  suc  y  e.  x
109, 6, 4wral 2455 . . . . 5  wff  A. y  e.  x  suc  y  e.  x
115, 10wa 104 . . . 4  wff  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )
1211, 3cab 2163 . . 3  class  { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
1312cint 3842 . 2  class  |^| { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
141, 13wceq 1353 1  wff  om  =  |^| { x  |  (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x ) }
Colors of variables: wff set class
This definition is referenced by:  dfom3  4588
  Copyright terms: Public domain W3C validator