How to write $\pi$ as a set in ZF?

Note that when we define the natural numbers we have a good sense of addition and multiplication (ordinal arithmetics), and from those we can define the operations on $\Bbb Z$ and $\Bbb Q$ and then by using Dedekind cuts construction we can extend these to $\Bbb R$ as well.

So we have that $\Bbb R$ has the operations $+,\cdot$ and they all satisfy all the things we know they do from the times we did mathematics without writing all the sets explicitly.

Now we can use these things to start and define anything else that we desire using the $+$ and $\cdot$ and whatnot as our stones. For example you can define $\pi$ to be the length of the semi-circle of radius $1$.

How do we do that? We define what is an integral, and a path integral, and so on. All from the sets which are addition and multiplication and so on, and then we can define $\pi$ in a painfully tedious way.

The whole point of using set theory, and in this case $\sf ZF$, as our foundation is that we can do things, once we can define the real numbers with their basic properties we have formulas which define things from that structure, and we don't have to write everything in set-form explicitly.

Once we have the real numbers (with the order) it is easy to define the collection of open intervals, and then it is easy to define the standard topology (the smallest collection containing the intervals and having certain properties), from there we can define the Borel sets, the Lebesgue sets, and the Lebesgue measure (being the unique function from the Lebesgue sets into the real numbers which satisfies certain properties), then we can define integration and with respect to the measure, and we can define derivation.

All these things end up being immensely long and complicated formulas, but the point is that we can write them up. And all this with just $\in$ and the axioms of $\sf ZF$. (Although we may want to add $\sf DC$ or even $\sf AC$ if we discuss measure theory.)

But if you do want to insist on $\pi$ being written in set form:

$$\pi = \left\{x\in\Bbb Q\mathrel{}\middle|\mathrel{} x<_\Bbb Q0\lor \left(x\geq_\Bbb Q0\land\exists k\in\Bbb N:\frac{x^2}6<_\Bbb Q\sum_{n=1}^k\frac1{n^2}\right)\right\}$$

Let me try this $$(\pi)_{\mathbb{R}}=\left\{x\in \mathbb{Q}:\;\exists k\in\mathbb{N}.\;x< \sum\limits_{n=0}^{k}\cfrac{2^{n+1} n!^2}{(2n + 1)!}\right\}$$ This would be the Dedekind construction of the reals, and note that there is no union here.

Or, I would complete the rationals first by taking the quotient of ring of fundamental sequences with maximal ideal of null sequences $\mathcal{F}_Q/\mathcal{N}_Q$ to obtain a complete field $\mathbb{R}$, then I can safely say that $$\pi=\lim\limits_{k\to\infty}\sum\limits_{n=0}^{k}\cfrac{2^{n+1} n!^2}{(2n + 1)!}$$ (or define exp first, then define sin, then define $\pi$)