## 2.5. The powerset

Let us extend set theory by 3 new symbols (powerset, exponentiation,
product) with axioms, that will declare given classes *C* to
be sets *K*. These extensions are similar to those provided by
the set generation principle (1.11), but no more satisfy its
requirement.

In the traditional ZF formalization of set theory only accepting ∈
as primitive stucture, such a declaration is done purely by the
axiom (or theorem) (∀ parameters), ∃*K*, ∀*x*, *x* ∈
*K* ⇔ *C*(*x*). Then, the operator symbol *K*
taking the parameters of *C* as its arguments, represents the
following abbreviations: ∀*x*∈*K* means ∀*x*, *C*(*x*)⇒
; the equality *X*=*K* means (∀*x*,
*x* ∈ *X* ⇔ *C*(*x*)),
and any other *A*(*K*) means
∃*X*, (*X*=*K*)∧*A*(*X*).
But these formulas use open quantifiers, forbidden in our framework.

For what the set generation principle justified, ∀_{C}
could be replaced by formulas, while the above ∃*X* could be
treated by existential elimination (1.9). But otherwise without open
quantifiers, even a given set *K* identical to a class *C*,
would not be recognizable as such, so that the very statement that *C*
coincides with a set remains practically meaningless.

Thus, our set theoretical framework requires the operator symbol *K*
to be regarded as primitive in the language (instead of a defined
abbreviation), with argument the tuple *y* of parameters of *C*,
and the axiom

(∀*y*…), Set(*K*(*y*))∧(∀*x*,
*x* ∈ *K*(*y*) ⇔ *C*_{y}(*x*))

**Powerset.** ∀_{Set} *E*, Set(℘(*E*))
∧ (∀*F*, *F*∈℘(*E*) ⇔ (Set(*F*) ∧ *F*
⊂ *E*))*. *

We shall also shorten ∈ ℘ into ⊂ in binders: (∀*A*⊂*E*,…) ⇔ (∀*A*∈℘(*E*),…).

**Exponentiation.** ∀_{Set} *E*,*F*,
Set(*F*^{E})∧(∀*f*, *f* ∈ *F*^{E} ⇔
*f* : *E* → *F*)*. *

**Product of a family of sets.** *This binder
generalizes the finite product operators (2.3):*

∀*x*, *x* ∈ ∏

*i*∈*I* *E*_{i}
⇔ (Fnc(*x*) ∧ Dom *x* = *I* ∧ ∀*i*∈*I*,
*x*_{i} ∈ *E*_{i}).

For all *i* ∈ *I*, the *i*-th projection is
the function π_{i} from ∏_{j∈I}
*E*_{j} to *E*_{i}
evaluating every family *x* at *i* : π_{i}(*x*)=*x*_{i}.
This is the function evaluator curried in the unnatural order.

These operators are «equivalent» in the sense that they are
definable from each other:

℘(*E*)={*f*^{•}(1) | *f*
∈ V_{2}^{E}}

*F*^{E}= ∏_{x∈E}* F* =
{(ϵ
⃗*R*(*x*))_{x∈E}
| *R* ⊂ *E*×*F* ∧ ∀*x*∈*E*, ∃!: ⃗*R*(*x*)}

{*x* ∈ (⋃

*i*∈*I* *E*_{i})^{I}|∀*i*∈*I*,
*x*_{i} ∈ *E*_{i}} =
{(ϵ ⃗*R*(*i*))_{i∈I}
| *R* ⊂ ∐

*i*∈*I*
*E*_{i} ∧ ∀*x*∈*E*, ∃!: ⃗*R*(*x*)}

Even some cases are expressible from previous tools:

*F*^{{a}}= {{*a*}∋*x*↦*y*
| *y* ∈ *F*}

*F*^{∅}= {∅}

℘({*a*}) = {∅,{*a*}}

∏

*i*∈*I*∪*J*
*E*_{i}={(*i*∈*I *? *x*_{i}
: *y*_{i})_{i∈I∪J}
| (*x*,*y*) ∈ ∏

*i*∈*I**E*_{i} × ∏

*i*∈*J**E*_{i}}

(∃*i*∈*I*, *E*_{i}=∅) ⇒ ∏

*i*∈*I**E*_{i} =∅

(∀*i*∈*I*, ∃!:*E*_{i}) ⇒ ∏

*i*∈*I**E*_{i}
= {(ϵ*E*_{i})_{i∈ I}}

If *F* ⊂ *F*′ then ℘(*F*) ⊂ ℘(*F*′), *F*^{E}
⊂ *F*′^{E}, and (∀*i*∈*I*, *E*_{i}
⊂ *E*′_{i}) ⇒ ∏_{i∈I} *E*_{i}
⊂ ∏_{i∈I} *E*′_{i} .

**Cantor's Theorem. **∀_{Set}
*E*, ∀_{Fnc} *f*, Dom *f* = *E* ⇒ ℘(*E*) ⊄ Im *f**. *

Proof: *F* = {*x*∈*E*| *x* ∉ *f*(*x*)}
⇒ (∀*x*∈*E*, *x* ∈ *F* ⇎ *x* ∈ *f*(*x*))
⇒ (∀*x*∈*E*, *F* ≠ *f*(*x*)) ⇒ *F*
∉ Im *f*.∎

(Russell's
paradox may be seen as a particular case)