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. And then any such formula_10 is itself a member of an even larger “almost universal set” and so on. It's one of the strong cardinality axioms guaranteeing vastly more sets than one normally assumes to exist.