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

Definition df-iom 4475
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 4260. 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 4476 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 4474 . 2  class  om
2 c0 3333 . . . . . 6  class  (/)
3 vx . . . . . . 7  setvar  x
43cv 1315 . . . . . 6  class  x
52, 4wcel 1465 . . . . 5  wff  (/)  e.  x
6 vy . . . . . . . . 9  setvar  y
76cv 1315 . . . . . . . 8  class  y
87csuc 4257 . . . . . . 7  class  suc  y
98, 4wcel 1465 . . . . . 6  wff  suc  y  e.  x
109, 6, 4wral 2393 . . . . 5  wff  A. y  e.  x  suc  y  e.  x
115, 10wa 103 . . . 4  wff  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x )
1211, 3cab 2103 . . 3  class  { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
1312cint 3741 . 2  class  |^| { x  |  ( (/)  e.  x  /\  A. y  e.  x  suc  y  e.  x
) }
141, 13wceq 1316 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  4476
  Copyright terms: Public domain W3C validator