Description: Define power class.
Definition 5.10 of [TakeutiZaring] p. 17,
but we
also let it apply to proper classes, i.e. those that are not members of
V. When applied to a set, this produces its power set. A
power
set of S is the set of all subsets of S, including the empty set and S
itself. For example, if A =
{ 3 , 5 , 7 }, then
℘A = {∅, {
3 }, { 5 }, { 7 }, { 3 , 5 },
{ 3 , 7 }, { 5 , 7 }, { 3 , 5
, 7 }} (ex-pw in
set.mm). We will later introduce the Axiom of Power Sets ax-pow in
set.mm, which can be expressed in class notation per pwexg 4328. Still
later we will prove, in hashpw in set.mm, that the size of the power set
of a finite set is 2 raised to the power of the size of the set.
(Contributed by NM, 5-Aug-1993.) |