Show that the powerset partial order is a cartesian closed category. I'm trying to get started learning category theory.  A problem I'm working on is to show that for a set $S$, the partial order $(\mathcal{P}(S),\subseteq)$ viewed as a category is cartesian closed. 

So far, I was thinking that $S$ is the terminal object, and that the product of any two subsets $A \times B$ always exists (the greatest lower bound or intersection of $A$ and $B$), but am having trouble completing the proof by showing that the category has exponentiation.

If I understand right, the goal is to show that for any $A$ and $B$, there is a $C$ such that $C \times A \to B$ (i.e., $(C \cap A) \subseteq B$) if and only if there is a $B^A$ such that $C \subseteq B^A$ and $(B^A \cap A) \subseteq B$. But then this doesn't seem quite right.

I'm sorry for such a beginner question. I'd really appreciate any help pointing me in the right direction or maybe clarifying what/how one would go about showing that this category has exponentiation - or what does "$B^A$" mean in terms of these subsets? Does some sequence of operations construct it?
Let's prove something stronger: every infinitary-distributive complete lattice is a complete Heyting algebra (and so cartesian closed as a category).

Recall, a complete lattice is a partial order in which all meets and joins exist. The powerset of a set is certainly a complete lattice, and it moreover satisfies the infinite distributive law:
$$\left( \bigcup_{i \in I} A_i \right) \cap B = \bigcup_{i \in I} (A_i \cap B)$$
Now the claim is that such a complete lattice has a Heyting operation, i.e. a binary operation $\to$ such that $A \subseteq (B \to C)$ if and only if $A \cap B \subseteq C$ for all $A$. How do we do this? Let's apply wishful thinking. Suppose we had such a $(B \to C)$; then $(B \to C) \subseteq (B \to C)$, and in particular, $(B \to C)$ must be the greatest $A$ such that $A \cap B \subseteq C$. On the other hand, we are in a complete lattice, so we can certainly define
$$(B \to C) = \bigcup \{ A : A \cap B \subseteq C \}$$
and this works: if $A \subseteq (B \to C)$, then 
$$A \cap B \subseteq (B \to C) \cap B = \left( \bigcup \{ A : A \cap B \subseteq C \} \right) \cap B = \bigcup \{ A \cap B : A \cap B \subseteq C \} \subseteq C$$
by the infinite distributive law; the converse is automatic by construction of $(B \to C)$.

The nice thing about this proof is that it is completely constructive and can be internalised in any topos. But in the classical setting, we can be a little bit more explicit about what $(B \to C)$ is: writing $B^{\mathsf{c}}$ for the complement of $B$, we have $(B \to C) = B^{\mathsf{c}} \cup C$. Clearly, $(B^{\mathsf{c}} \cup C) \cap B = C \cap B \subseteq C$, so $(B^{\mathsf{c}} \cup C) \subseteq (B \to C)$; on the other hand, if $A \cap B \subseteq C$, then $B^{\mathsf{c}} \cup (A \cap B) \subseteq B^{\mathsf{c}} \cup C$, and clearly
$$A = A \cap (B^{\mathsf{c}} \cup B) = (A \cap B^{\mathsf{c}}) \cup (A \cap B) \subseteq B^{\mathsf{c}} \cup (A \cap B)$$
so $A \subseteq B^{\mathsf{c}} \cup C$, and therefore $(B \to C) \subseteq B^{\mathsf{c}} \cup C$, as required. (Exercise: Where have I used the law of excluded middle in this argument?)
I found this question in Pierce's book and have been working on it today. Here's what I've got:

The Problem: The exponent $B^A$ needs to be a member of the powerset. Moreover it has to satisfy the following constraints:


There is a map from $B^A \times A$ to $B$.

in terms of sets, $B^A \times A \subseteq B$

For every other powerset object $C$ such that $g: C \times A \rightarrow B$ exists, we need a unique map from $C$ to $B$ 

again in terms of sets, we must show that for all $C$ such that $C \times A \subseteq B$, the relation $C \subseteq B$ must hold.



Solution: If $B \subset A$ then $B^A = B$. Otherwise $B^A = S$ (the final object in our powerset category).

Justification: If $B \subset A$ then $B^A$ must be a subset of $B$ for $B^A \times A \subseteq B$ to hold. We deduce that $B^A$ must be $B$ exactly because it is the only choice that guarantees $C \subseteq B^A$ for every $C$ such that $C^A \times A \subseteq B$.

If $A \subseteq B$ then $B^A \times A \subseteq B$ holds for any choice of $B^A$. Likewise, we can use any powerset element $C$ to satisfy $C^A \times A \subseteq B$. Because of this, $B^A$ has to be the entire set $S$. It is the only choice that guarantees $C \subseteq B^A$ for every valid choice of $C$.