Proof of The Number n Lies in the Segment [n], and Membership in the Addition Class on ω

Throughout, set-builder classes such as $\{k\in\mathbb{N}:k\le n\}$ are restricted class abstractions of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii), as Sets and Maps: Ordinary Notation (iii) provides; ordered pairs of sets are sets by The Ordered Pair of Two Sets and Nested Tuples (i); and $m+n$ is a set for $m,n\in\omega$ by Addition on Omega (i).

Proof of (i). Let $n\in\mathbb{N}$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i),

$$[n]=\{k\in\mathbb{N}:k\le n\},$$

so by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), $n\in[n]$ if and only if $n\in\mathbb{N}$ and $n\le n$. The first condition holds by assumption, and $n\le n$ holds by Arithmetic and Order of the Natural Numbers (vi). Hence $n\in[n]$.

Proof of (ii). Let $a$, $b$ and $c$ be sets. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), applied to the class $+$ of Addition on Omega (i), $((a,b),c)\in{+}$ if and only if there are $m,n\in\omega$ with

$$((a,b),c)=((m,n),m+n).$$

By The Characteristic Property of Ordered Pairs and Nested Tuples of Sets (i), applied first to these two pairs and then to $(a,b)=(m,n)$, this equation holds if and only if $a=m$, $b=n$ and $c=m+n$. Hence, if $((a,b),c)\in{+}$, then $a\in\omega$, $b\in\omega$ and $c=a+b$; conversely, if $a,b\in\omega$ and $c=a+b$, the witnesses $m=a$ and $n=b$ give $((a,b),c)\in{+}$.

The argument for (ii) is adapted from the published proof (proof version ea2a2f1d-b7b8-4793-97f8-76d3456bac36) of the membership clause of lem:omega-multiplication-values-2026a (theorem version 8920386c-768d-45bd-8ead-a57505afa932).