Proof of The Index Map Skipping One Element of [n]

Each result cited is universally quantified over the data in its own statement. Write $m=n-1$. For $q\in\mathbb{N}_{0}$, the elements of $[q]$ are the $k\in\mathbb{N}$ with $k\le q$. By Arithmetic and Order of the Natural Numbers §successor and trichotomy, for $p,q\in\mathbb{N}$ with $p<q+1$ we have $p\le q$.

Clause difference. By The Difference of Two Natural Numbers with Zero §difference, $m$ is the element of $\mathbb{N}_{0}$ with $1+m=n$. If $m=0$, then $n=1<2$, contrary to $2\le n$. So $m\in\mathbb{N}_{0}\setminus\{0\}=\mathbb{N}$, and $m+1=1+m=n$.

(P) For $k\in[m]$: $k\in[n]$ and $k+1\in[n]$, since $k\le m<m+1=n$ and $k+1\le m+1=n$.

Clause map. By (P), Maps Defined by Cases §cases, with the sets $[m]$ and $[n]$, the property $k<i$ and the expressions $k$ and $k+1$, gives exactly one map $s:[m]\to[n]$ with $s(k)=k$ for every $k\in[m]$ with $k<i$ and $s(k)=k+1$ for every $k\in[m]$ for which $k<i$ fails. For $k\in[m]$, $k<i$ fails if and only if $i\le k$, by trichotomy. So the maps described in clause map are exactly those described in Maps Defined by Cases §cases, and there is exactly one. From now on $s$ is this map.

Clause increasing. Let $k,l\in[m]$ with $k<l$. If $l<i$, then $s(k)=k<l=s(l)$. If $k<i\le l$, then $s(k)=k<l<l+1=s(l)$. If $i\le k$, then $i\le l$ and $s(k)=k+1<l+1=s(l)$. So $s(k)<s(l)$. Conversely, let $s(k)<s(l)$. If $k<l$ failed, then $k=l$ or $l<k$, so $s(k)=s(l)$ or, by what was just shown, $s(l)<s(k)$; both contradict $s(k)<s(l)$. Hence $k<l$.

Clause range. Let $k\in[m]$. If $k<i$, then $s(k)=k\neq i$; if $i\le k$, then $i<k+1=s(k)$. So $s(k)\in[n]\setminus\{i\}$, and $s$ is a map $s:[m]\to[n]\setminus\{i\}$.

Injectivity. If $k,l\in[m]$ and $k\neq l$, then $k<l$ or $l<k$, so $s(k)\neq s(l)$ by clause increasing. Thus $s$ is injective by Injective, Surjective and Bijective Functions between Classes §injective.

Surjectivity. Let $p\in[n]\setminus\{i\}$, so $p\in\mathbb{N}$, $p\le n$ and $p<i$ or $i<p$. If $p<i$, then $p<i\le n=m+1$, so $p\le m$; thus $p\in[m]$ and $s(p)=p$. If $i<p$, then $1\le i<p$, so $p\neq1$ and, by Arithmetic and Order of the Natural Numbers §predecessor, $p=d+1$ for some $d\in\mathbb{N}$. Then $i<d+1$ gives $i\le d$, and $d+1=p\le m+1$ gives $d\le m$; so $d\in[m]$ and $s(d)=d+1=p$. Hence $s:[m]\to[n]\setminus\{i\}$ is surjective by Injective, Surjective and Bijective Functions between Classes §surjective, and a bijection by Injective, Surjective and Bijective Functions between Classes §bijective.