the slice category , where Inj? is the wide subcategory of Set with morphisms restricted to injections. This is similar to the subobject definition but is more unpacked. has objects that are injections to and morphisms that are commuting triangles of injections.
If is a set, then there exists a set such that if .
One can then use the axiom of separation (bounded separation is enough) to prove that may be chosen so that the subsets of are the only members of ; the axiom of extensionality proves that this is unique.
In predicative mathematics, the existence of power sets (along with other “impredicative” axioms) is not accepted. However we can still speak of a power set as a proper class, sometimes called a power class.
One can use power sets to construct function sets; the converse also works using excluded middle (or anything else that will guarantee the existence of the set of truth values). In particular, power sets exist in any theory containing excluded middle and function sets; thus predicative theories which include function sets must also be constructive.
in the usual arithmetic of cardinal numbers.
Power sets live in the category Set. Given an object of any category, one can similarly form a poset of subobjects of ; the category is called well-powered when this poset is small. One also has an internal notion of power set (a power object) in a topos.
The power set construction constitutes an equivalence of categories between the opposite category Set and that of complete atomic Boolean algebras. See at Set – Properties – Opposite category and Boolean algebras. Restricted to finite sets, the power set construction constitutes an equivalence of categories between the opposite category of FinSet and that of finite Boolean algebras. See at FinSet – Opposite category.