 That formula_10 looks much like a “universal set” for formula_7 – it not only has as members the powerset of formula_7, and all subsets of formula_7, it also has the powerset of that powerset and so on – its members are closed under the operations of taking powerset or taking a subset.It's like a “universal set” except that of course it is not a member of itself and is not a set of all sets.That's the guaranteed Grothendieck universe it belongs to.