This paper is about two topics: 1. systems of explicit mathematics with universes and a non-constructive quantification operator $\mu$; 2. iterated fixed point theories with ordinals. We give a proof-theoretic treatment of both families of theories; in particular, ordinal theories are used to get upper bounds for explicit theories with finitely many universes.