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

Definition df-iom 4341
 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 4132. 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 4342 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 4340 . 2
2 c0 3251 . . . . . 6
3 vx . . . . . . 7
43cv 1258 . . . . . 6
52, 4wcel 1409 . . . . 5
6 vy . . . . . . . . 9
76cv 1258 . . . . . . . 8
87csuc 4129 . . . . . . 7
98, 4wcel 1409 . . . . . 6
109, 6, 4wral 2323 . . . . 5
115, 10wa 101 . . . 4
1211, 3cab 2042 . . 3
1312cint 3642 . 2
141, 13wceq 1259 1
 Colors of variables: wff set class This definition is referenced by:  dfom3  4342
 Copyright terms: Public domain W3C validator