Definition power_eq

Definition. power_eq
power M = {A | A ⊆ M}

The power set of a set is the set of all its subclasses. According to the axiom of power sets it can never be a proper class. One could consider powers of proper classes. The power of the universal class is the universal class itself, as shown in power_UnivCl. This strange behavior can be explained in terms of universes. The true power, that is power M, is replaced by a truncated version U ∩ power M where U is a universe, a set with M ⊆ U that resembles the universal class. Under these circumstances, we observe truncated_power_closed and truncated_power_idem.