Unrestricted finite colourings and used palettes

Let $X$ be a finite set, meaning a set in bijection with a natural number, and let $k$ be a nonzero natural number. Write $[k]=\{1,\dots ,k\}=\{i\in \sigma (k):i\mathrm{\ne }0\}$, where $\sigma (k)=k\cup \{k\}$ is the successor of $k$. A $k$-colouring of $X$ is any function $c:X\to [k]$: it assigns exactly one member of $[k]$ to each element of $X$.

The used palette is $c[X]=\{i\in [k]:\mathrm{\exists }x\in Xc(x)=i\}$. For $i\in [k]$, its colour class, or fibre, is $c^{-1}(\{i\})=\{x\in X:c(x)=i\}$. A subset $Y\subseteq X$ is monochromatic if $c(x)=c(y)$ for every $x,y\in Y$; in particular, the empty subset is monochromatic. Colours need not all be used. When $X$ is a graph's vertex set, this definition imposes no restriction on the colours of adjacent vertices.

The natural-number supplier gives $\sigma (k)$ as a set. Separation applied within it gives $[k]$; applied within $[k]$ and $X$, respectively, it also gives the displayed used palette and each colour class. Extensionality makes each of these sets unique by its stated members. The function definition supplies the unique value $c(x)$ for every $x\in X$, so the equality conditions are unambiguous. The monochromatic condition is a definite predicate, including when $Y$ is empty.

A function is a relation f with (a,b) ∈ f and (a,c) ∈ f implying b = c; f : A → B, the value f(a), domain and codomain

The cardinality | A| of a finite set

The natural numbers ℕ (von Neumann)

The Axiom Schema of Separation: for each formula φ, ∀ p̄ ∀ x ∃ y ∀ z (z ∈ y ↔ (z ∈ x ∧ φ(z,p̄)))

The Axiom of Extensionality: ∀ x ∀ y (∀ z (z ∈ x ↔ z ∈ y) → x = y)

A finite simple graph is a finite vertex set together with a set of two-element vertex subsets