Proof of Images of Finite Sets Are Finite, Bounded Sets of Natural Numbers Are Finite, and Nonempty Finite Totally Ordered Sets Have Extreme Elements

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Formulas. The clauses image and extremes are proved by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction, applied to predicative formulas $\varphi$ in which its set variable $A$ is free; to keep the letters apart, the sets $A$, $B$ and $X$ of the statement are written $A_{0}$, $B_{0}$ and $X_{0}$ below. The letters $d$, $t$, $u$, $v$, $w$ and $z$ denote set variables, distinct from each other and from $A$, and $F$, $Q$, $R$, $X$, $Y$ and $Z$ distinct class variables. The formula $\mathrm{fin}(z)$ is that of Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §predicative with $z$ as its set variable and the class variables $X$, $Y$ and $R$, assigned $\mathbb{N}_{0}$, $\mathbb{N}$ and $\le$; it is predicative, and it holds if and only if the value of $z$ is finite.

Images. Let $A_{0}$ be finite and $f:A_{0}\to B_{0}$ a map; so $f$ is a function with $\operatorname{dom}f=A_{0}$ by Functions, Values of a Function, and Functions from One Class to Another §map, and by Sets and Maps: Ordinary Notation §images its image $f(A_{0})$ is the image $f[A_{0}]$ of The Image and the Preimage of a Class under a Class §image. Let $\theta(z,A,F)$ be $\forall w\,(w\in z\Leftrightarrow\exists u\,(u\in A\wedge(u,w)\in F))$, predicative since $(u,w)\in F$ is by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership and only set variables are quantified. Let $\gamma(A)$ be $A\subseteq d\wedge\Phi(F)$, where $A\subseteq d$ abbreviates the predicative formula $\forall u\,(u\in A\Rightarrow u\in d)$ of Subclasses and Subsets §subclass, and $\Phi(F)$ is the predicative formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §function, which holds if and only if $F$ is a function. For every set $C$ and every function $F$, the image $F[C]$ is a set by Images of Sets under Functions Are Sets, and a Function with a Set Domain Is a Set §image-set, and by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §class-terms, applied to the class abstraction of The Image and the Preimage of a Class under a Class §image, it is the only set $z$ satisfying $\theta(z,C,F)$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §elimination, with $k=1$, $v_{1}=A$, the parameters $d$, $F$, $X$, $Y$ and $R$, and $\mathrm{fin}(z)$ as the formula there called $\varphi$, the formula $\varphi(A)$ given by $\gamma(A)\Rightarrow\forall z\,(\theta(z,A,F)\Rightarrow\mathrm{fin}(z))$ is predicative; assigning $A_{0}$ to $d$ and $f$ to $F$, where $\Phi(f)$ holds as $f$ is a function, for every set $C$ the formula $\varphi(C)$ holds if and only if $C\subseteq A_{0}$ implies that $f[C]$ is finite. The image $f[\emptyset]$ has no element by The Image and the Preimage of a Class under a Class §image, so it is $\emptyset$, finite by The Pigeonhole Principle, Uniqueness of the Length of a Finite Set, and the Finiteness of the Empty Set and of Singletons §small. Let $C$ be finite with $\varphi(C)$, let $x\notin C$, and let $C\cup\{x\}\subseteq A_{0}$. Then $C\subseteq A_{0}$, so $f[C]$ is finite, and $x\in\operatorname{dom}f$, so by Functions, Values of a Function, and Functions from One Class to Another §value $f(x)$ is the only set $v$ with $(x,v)\in f$. Hence, by The Image and the Preimage of a Class under a Class §image, the elements of $f[C\cup\{x\}]$ are those of $f[C]$ together with $f(x)$, that is, $f[C\cup\{x\}]=f[C]\cup\{f(x)\}$, which is finite by Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite §insert. So $\varphi(C\cup\{x\})$ holds, and by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction $\varphi(C)$ holds for every finite set $C$. Taking $C=A_{0}$, the image $f(A_{0})=f[A_{0}]$ is finite. This is the clause image for $A=A_{0}$ and $B=B_{0}$.

Extreme elements. Let $\le$ be a total order on a set $X_{0}$. Let $\varphi(A)$ be

$$(A\subseteq Z\wedge\exists w\,(w\in A))\Rightarrow\bigl(\exists t\,(t\in A\wedge\forall v\,(v\in A\Rightarrow(v,t)\in Q))\wedge\exists t\,(t\in A\wedge\forall v\,(v\in A\Rightarrow(t,v)\in Q))\bigr),$$

with the parameters $Z$ and $Q$. It is predicative: $A\subseteq Z$ abbreviates the predicative formula of Subclasses and Subsets §subclass, $(v,t)\in Q$ and $(t,v)\in Q$ are predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership, and only set variables are quantified. Assign $X_{0}$ to $Z$ and the relation $\le$ to $Q$; then $(v,t)\in Q$ holds if and only if $v\le t$, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity §pair-membership and Partial and Total Orders on a Set and the Associated Strict Relation §partial, so for every set $C$, $\varphi(C)$ says: if $C\subseteq X_{0}$ and $C\neq\emptyset$, then $C$ has a greatest element and a least element in the sense of Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least. As $\emptyset$ has no element, $\varphi(\emptyset)$ holds. Let $C$ be finite with $\varphi(C)$, let $x\notin C$, and let $S=C\cup\{x\}\subseteq X_{0}$; so $C\subseteq X_{0}$ and $x\in X_{0}$. The order is reflexive and transitive by Partial and Total Orders on a Set and the Associated Strict Relation §partial. If $C=\emptyset$, then $S=\{x\}$ and $x\le x$, so $x$ is the greatest and the least element of $S$. Otherwise $C$ has a greatest element $M'$ and a least element $m'$. By Partial and Total Orders on a Set and the Associated Strict Relation §total, $M'\le x$ or $x\le M'$; let $M=x$ if $M'\le x$, and $M=M'$ otherwise, so that then $x\le M'$. Then $M\in S$; $M'\le M$ (by the case assumption if $M=x$, by reflexivity if $M=M'$), and $x\le M$ (by reflexivity if $M=x$, by the case assumption if $M=M'$); and for $v\in C$, $v\le M'\le M$ gives $v\le M$ by transitivity. So $M$ is a greatest element of $S$; in the same way, with the inequalities reversed, $x$ or $m'$ is a least element of $S$. So $\varphi(C\cup\{x\})$ holds, and by Induction over Finite Sets, and Predicative Formulas for the Segments [n] and for Finiteness §induction $\varphi(C)$ holds for every finite set $C$. Hence every nonempty finite subset $S$ of $X_{0}$ has a greatest and a least element, denoted $\max S$ and $\min S$ by Bounds, Least and Greatest Elements, Suprema and Infima for a Partial Order §least. This is the clause extremes for $X=X_{0}$.

Bounded sets of natural numbers. Let $S\subseteq\mathbb{N}_{0}$, and let $b\in\mathbb{N}_{0}$ with $k\le b$ for every $k\in S$. Since $0\le k$ for every $k\in\mathbb{N}_{0}$, $S\subseteq\{0,\dots,b\}$ by Intervals of Natural Numbers §interval. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting §shift, with $0$, $b$ and $1$ in place of $m$, $n$ and $p$, the map $k\mapsto k+1$ is a bijection from $\{0,\dots,b\}$ onto $\{0+1,\dots,b+1\}=\{1,\dots,b+1\}$, which is $[b+1]$ by Intervals of Natural Numbers §segment. Its inverse is a bijection from $[b+1]$ onto $\{0,\dots,b\}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §inverse, so $\{0,\dots,b\}$ is finite by Finite Sets §finite, and $S$ is finite by Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite §subset. Conversely, let $S$ be finite. If $S=\emptyset$, then $b=0$ serves. Otherwise, the order of $\mathbb{N}_{0}$ is a well-order by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order, hence a total order on $\mathbb{N}_{0}$ by Well-Orders on a Set §well-order, so $S$ has a greatest element $\max S$ by the clause extremes, applied with $\mathbb{N}_{0}$ in place of $X$, and $b=\max S$ serves. Finally, an interval $\{m,\dots,n\}$ with $m,n\in\mathbb{N}_{0}$ is a subset of $\mathbb{N}_{0}$ all of whose elements are at most $n$, by Intervals of Natural Numbers §interval, so it is finite. This proves the clause naturals.