===== Power set =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $X$ ... set |
| @#FFBB00: definiendum | @#FFBB00: $ Y \in \mathcal{P}(X) $ |
| @#55EE55: postulate   | @#55EE55: $ Y\subseteq X $ |

-----
Here we define

$\mathcal{P}(X) \equiv \{Y\mid Y\subseteq X\}$

which is sensible in our set theory if, for each set $X$, we have

$\exists! P.\,P = \{Y\mid Y\subseteq X\}$

or, more formally,

$\forall X.\,\exists! P.\,P = \{Y\mid Y\subseteq X\}$

which is short for

$\forall X.\,\exists! P.\,\forall Y.\,\left(Y\in P\Leftrightarrow Y\subseteq X\right)$

=== Discussion ===
The above is short for

$\forall X.\,\exists! P.\,\forall Y.\,\left(Y\in P\Leftrightarrow \forall Z.\,(Z\in Y\implies Z\in X)\right)$

and this is, apart from the exclamation mark,exactly the [[https://en.wikipedia.org/wiki/Axiom_of_power_set|Axiom of power set]].

Like in the case of the [[empty set]], uniqueness follows from extensionality.

== Examples ==
We can prove

$\forall Y.\,\left(Y\in \{\emptyset\}\leftrightarrow Y\subseteq \emptyset\right)$

Therefore, for $X$ being $\emptyset$, we can show that the job of $P$ is done by $\{\emptyset\}$. 
In other words

^ $\mathcal{P}(\emptyset)=\{\emptyset\}$ ^ 

== Remarks ==
Generally, $\emptyset\in\mathcal{P}(X)$ for any $X$. Hence no power set is empty. 

One also writes $ \mathcal{P}(X) \equiv 2^X\equiv\Omega^X  $.

=== Reference ===
Wikipedia:
[[https://en.wikipedia.org/wiki/Axiom_of_power_set|Axiom of power set]]

-----
=== Context ===
[[Sets]]