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

Definition df-iom 4508
 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 4293. Later, when we define complex numbers, we will be able to also define a subset of the complex numbers (df-inn 8740) 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 7062. (Contributed by NM, 6-Aug-1994.) Use its alias dfom3 4509 instead for naming consistency with set.mm. (New usage is discouraged.)
Assertion
Ref Expression
df-iom
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-iom
StepHypRef Expression
1 com 4507 . 2
2 c0 3363 . . . . . 6
3 vx . . . . . . 7
43cv 1330 . . . . . 6
52, 4wcel 1480 . . . . 5
6 vy . . . . . . . . 9
76cv 1330 . . . . . . . 8
87csuc 4290 . . . . . . 7
98, 4wcel 1480 . . . . . 6
109, 6, 4wral 2416 . . . . 5
115, 10wa 103 . . . 4
1211, 3cab 2125 . . 3
1312cint 3774 . 2
141, 13wceq 1331 1
 Colors of variables: wff set class This definition is referenced by:  dfom3  4509
 Copyright terms: Public domain W3C validator