Proof of The Integers Lying in a Bounded Real Interval Form a Finite Set

The order of $\mathbb{Z}$ read in $\mathbb{R}$. For $n,n'\in\mathbb{Z}$: $n\le n'$ if and only if $\kappa(j(n))\le\kappa(j(n'))$. Indeed $n\le n'$ if and only if $j(n)\le j(n')$, by The Rational Numbers Form an Archimedean Ordered Field Containing the Integers (ii). For $u,v\in\mathbb{Q}$, $u\le v$ means $u<v$ or $u=v$, and likewise in $\mathbb{R}$, $<$ being the strict relation of a reflexive order (Partial and Total Orders on a Set and the Associated Strict Relation (iii)); if $u<v$, then $\kappa(u)<\kappa(v)$, and if $\kappa(u)<\kappa(v)$, then $u<v$, by The Rational Numbers Embed in Exactly One Way into Every Ordered Field (iv); and $\kappa(u)=\kappa(v)$ implies $u=v$ as $\kappa$ is injective (The Rational Numbers Embed in Exactly One Way into Every Ordered Field (iii)). So $u\le v$ if and only if $\kappa(u)\le\kappa(v)$, and the claim follows with $u=j(n)$ and $v=j(n')$.

A finite set of integers. Let $p=\lfloor a\rfloor$ and $q=\lfloor b\rfloor$ be the integer parts of $a$ and $b$, integers, with $\kappa(j(p))\le a$ by The Integer Part of a Real Number (i), an integer $n$ being read in $\mathbb{R}$ as $\kappa(j(n))$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (v)). Let $S=\{n\in\mathbb{Z}:p\le n\le q\}$, a subset of $\mathbb{Z}$. If $p\le q$, then $S$ is finite by The Number of Integers between Two Integers (i). Otherwise $S=\emptyset$: an $n\in S$ would give $p\le q$, as $\le$ is a total order on $\mathbb{Z}$ (The Integers Form an Ordered Ring Containing the Natural Numbers as Its Positive Elements (ii)); and $\emptyset$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iii).

The set $E$. Let $g=\kappa\circ j:\mathbb{Z}\to\mathbb{R}$, a map with $g(n)=\kappa(j(n))$ for every $n\in\mathbb{Z}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), and let $g|_{S}:S\to\mathbb{R}$ be its restriction, a map with $g|_{S}(n)=g(n)$ for $n\in S$ by Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii). Its image $E'=g|_{S}[S]$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vi), and $E'\subseteq\mathbb{R}$. Let $E=\{u\in E':a\le u\le b\}$, a subset of $E'$ and so a finite subset of $\mathbb{R}$ by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iv).

The elements of $E$. Let $u\in\mathbb{R}$. If $u\in E$, then $u\in E'$, so $u=g|_{S}(n)=\kappa(j(n))$ for some $n\in S\subseteq\mathbb{Z}$, and $a\le u\le b$. Conversely, let $u=\kappa(j(n))$ with $n\in\mathbb{Z}$ and $a\le u\le b$. Then $\kappa(j(p))\le a\le\kappa(j(n))$, so $p\le n$ by the first paragraph; and $\kappa(j(n))\le b$, so $\kappa(j(n))\le\kappa(j(q))$ by The Integer Part as the Greatest Integer Below, the Integer Part of a Double, and Powers of Two (i), applied to $z=b$, and $n\le q$ by the first paragraph. Hence $n\in S$, $u=g|_{S}(n)\in E'$, and, as $a\le u\le b$, $u\in E$.