|Description: Define power class.
Definition 5.10 of [TakeutiZaring] p. 17,
also let it apply to proper classes, i.e. those that are not members of
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 3 , 5 , 7 , then
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.)|