2.5. The powerset axiom

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, xK ⇔ C(x). Then, the operator symbol K taking the parameters of C as its arguments, represents the following abbreviations: ∀xK means ∀x, C(x)⇒ ; the equality X=K means (∀x, xX ⇔ 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 claim 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, xK(y) ⇔ Cy(x))

Powerset. Set E, Set(℘(E)) ∧ (∀F, F∈℘(E) ⇔ (Set(F) ∧ FE)).
We shall also shorten ∈ ℘ into ⊂ in binders: (∀AE,…) ⇔ (∀A∈℘(E),…).

Exponentiation.Set E,F, Set(FE)∧(∀f, fFE ⇔ f : EF).

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

x, x
Ei ⇔ (Fnc(x) ∧ Dom x = I ∧ ∀iI, xiEi).
For all iI, the i-th projection is the function πi from ∏jI Ej to Ei evaluating every family x at i : πi(x)=xi. 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) | fV2E}
FE= ∏xE F = {(ϵ R(x))xE | RE×F ∧∀xE, ∃!: R(x)}
 Ei)I|∀iI, xiEi} = {(ϵ R(i))iI | R
Ei ∧∀xE, ∃!: R(x)}
Even some cases are expressible from previous tools:

F{a}= {{a}∋xy | yF}
 F= {∅}
℘({a}) = {∅,{a}}
Ei={(iI ? xi : yi)iIJ | (x,y) ∈
(∃iI, Ei=∅) ⇒
Ei =∅ 
(∀iI, ∃!:Ei) ⇒
Ei = {(ϵEi)iI}

If FF′ then ℘(F) ⊂ ℘(F′), FEFE, and (∀iI, EiEi) ⇒ ∏iI Ei ⊂ ∏iI Ei .

Cantor Theorem. Set E, ∀Fnc f, Dom f = E ⇒ ℘(E) ⊄ Im f.
Proof: F = {xE| xf(x)} ⇒ (∀xE, xFxf(x)) ⇒ (∀xE, Ff(x)) ⇒ FIm f.∎
(The Russell paradox may be seen as a particular case)

Set theory and Foundations of Mathematics

1. First foundations of mathematics
2. Set theory (continued)
2.1. Tuples, families
2.2. Boolean operators on families of sets
2.3. Products, graphs and composition
2.4. Uniqueness quantifiers, functional graphs
2.5. The powerset axiom
2.6. Injectivity and inversion
2.7. Properties of binary relations on a set ; ordered sets
2.8. Canonical bijections
2.9. Equivalence relations and partitions
2.10. Axiom of choice
2.11. Notion of Galois connection
3. Model theory