Proof of The Segments [n]: Each Is a Set, and 1 Lies in [n] for n ∈ ℕ

Unfolding $[n]$. Let $n\in\mathbb{N}_{0}$. We have $1\in\mathbb{N}_{0}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n §one, so by Intervals of Natural Numbers §segment and Intervals of Natural Numbers §interval, applied with $m=1$,

$$[n]=\{1,\dots,n\}=\{k\in\mathbb{N}_{0}:1\le k\le n\}.$$

By The Order on Omega §order, $1\le k$ and $k\le n$ mean $(1,k)\in{\le}$ and $(k,n)\in{\le}$, a formula that quantifies over no class variables (its parameters are $\le$, $1$ and $n$), so this property of the elements $k$ of $\mathbb{N}_{0}$ is expressed as Sets and Maps: Ordinary Notation §set-builder requires. By that clause, in force by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §base, the class above is the restricted class abstraction of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted, namely $\{k:k\in\mathbb{N}_{0}\wedge 1\le k\le n\}$. An element of $[n]$ or of $\mathbb{N}_{0}$ is a set, so by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, for every $k$ in $[n]$ or in $\mathbb{N}_{0}$,

$$k\in[n]\iff k\in\mathbb{N}_{0}\text{ and }1\le k\text{ and }k\le n.\qquad(\ast)$$

Clause set. Let $n\in\mathbb{N}_{0}$. Now $\mathbb{N}_{0}$ is the set $\omega$ of natural numbers with zero, a set by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §set, as stated in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets. So $[n]=\{k\in\mathbb{N}_{0}:1\le k\le n\}$ is of the form treated in Sets and Maps: Ordinary Notation §set-builder with $A=\mathbb{N}_{0}$, and is a set by that clause. For every element $k$ of $[n]$, $(\ast)$ gives $k\in\mathbb{N}_{0}$; hence $[n]\subseteq\mathbb{N}_{0}$ by Subclasses and Subsets §subclass.

Clause one. Let $n\in\mathbb{N}$. Then $n\in\mathbb{N}_{0}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n §naturals, so $[n]$ is defined and $(\ast)$ holds, and $1\in\mathbb{N}_{0}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n §one, so $(\ast)$ applies to $k=1$. By Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one, $1\in\mathbb{N}$ and $1\le m$ for every $m\in\mathbb{N}$; applied to $m=1$ and $m=n$ this gives $1\le1$ and $1\le n$. Here $\le$ is the order of $\mathbb{N}_{0}$ as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, the one in Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication. Hence $1\in[n]$ by $(\ast)$.