Lifting up the proof theory to the countables : Zermelo-Fraenkel set theory

We describe the countable ordinals in terms of iterations of Mostowski collapsings. This gives a proof-theoretic bound of definable countable ordinals in the Zermelo-Fraenkel’s set theory ZF.