Definition·D029
Order on the naturals
Less-than is membership: each number is the set of all smaller ones.
for
(the naturals).
In words
m is less than n exactly when m is a member of n; and m is at most n exactly when it is less than n or equal to it.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
In the von Neumann coding a natural is the set of all smaller naturals (
), so comparison costs nothing: it is membership. As a set, the relation is
by Separation on the product, a relation on
. Its laws are inherited from the structure of the naturals: irreflexivity from regularity, transitivity from transitivity of each natural (both in L15), totality from trichotomy, and the interaction with arithmetic from L17 and L18. The crowning property is well-ordering.