Set theory (containing Power Set) Need Help in a proof I am confirming whether my proof is correct or not and need help.
     If  $ A \subseteq 2^A , $ then $  2^A \subseteq 2^{2^A} $
Proof:
Given: $ \forall x ($ $ x\in A \rightarrow \exists S $ where $ S \in 2^A  \wedge x \in S )$   --($0$)
Goal: $ \forall S  \forall x  ( $  $ S\in 2^A \wedge x \in S  \rightarrow \exists F $ such that  $F \in 2^{2^A} \wedge \exists S' $ such that $  S' \in$  $F \wedge x \in S')$
$  \forall S  \forall x \text { }S \in 2 ^A  \wedge x \in S $ adding to the given.               -(1)
New Goal: $\exists F $ such that $F \in 2^{2^A} \wedge \exists S' $ such that $  S' \in$  $F \wedge x \in S' $
By universal instantiation (1) ,
$ A \in 2 ^A  \wedge  x  \in  A $
From the above step we have $x \in A$, Hence,
By existential instantiation ($0$) ,
 $ A \in 2 ^A \wedge x \in A  $
Now I am taking negation of the new goal. (Proof by contradiction)
$\exists F  \text { such that } F \in 2^{2^A} \rightarrow  \exists S ' \text { such that } S'  \in F \rightarrow x \not \in S' $
  --($2$)
By existential instantiation of $F$ and $S'$ in ($2$)
 $F_0 \in 2^{2^A} \rightarrow A \in F_0 \rightarrow x \not\in A $
S' should be A.
How would I prove that $F_0 \in 2^{2^A}$
PS: Guidance using rule of inference is much appreciated.
 A: Here’s how I would write up a proof of this result.

Suppose that $X\in 2^A$; I need to show that $X\in 2^{2^A}$. Since $X\in 2^A$, I know that $X\subseteq A$. Let $x\in X$; then $x\in A\subseteq 2^A$, so $x\in 2^A$. Thus, $X\subseteq 2^A$, and hence by definition $X\in 2^{2^A}$.

In your argument I would first, for the sake of clarity, say that the initial goal is to show that for each $S\in 2^A$, $S\in 2^{2^A}$. This translates to showing that for each $S\in 2^A$, $S\subseteq 2^A$, or
$$\forall S\,\forall x\Big(S\in 2^A\land x\in S\to x\in 2^A\Big)\;.$$
Use univeral instantiation to get $S\in 2^A\land x\in S$. Your goal now is to show that $x\in 2^A$, which can be rewritten as $x\subseteq A$, or
$$\forall y\Big(y\in x\to y\in A\Big)\;.\tag{1}$$
Universal instantiation lets you write $y\in x$. From $S\in 2^A$ we get $\forall z(z\in S\to z\in A)$ which, when combined with $x\in S$, yields $x\in A$. Now recall that we were given $A\subseteq 2^A$, i.e., $\forall z(z\in A\to z\in 2^A)$, and we have $x\in A$, so $x\in 2^A$, which is essentially the new goal $(1)$.
Not being familiar with the specific system of inference that you’re using, I’ve left a lot of the logical details to you, but perhaps this is enough of a semi-formal expansion to point you in the right direction.
A: Here is how I would write down this proof, in a way which makes clear the inherent symmetry.  (Ignore the red coloring for now, I will use that below.)$
\newcommand{\calc}{\begin{align} \quad &}
\newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}}
\newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} }
\newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & }
\newcommand{\endcalc}{\end{align}}
\newcommand{\ref}[1]{\text{(#1)}}
\newcommand{\then}{\Rightarrow}
\newcommand{\followsfrom}{\Leftarrow}
\newcommand{\true}{\text{true}}
\newcommand{\false}{\text{false}}
\newcommand{\P}[1]{2^{#1}}
$

For every $\;X\;$, we have
$$\calc
  X \in \P{A}
\op\equiv\hint{definition $\ref 0$ of $\;\P{\cdots}\;$}
  X \subseteq A
\op\then\hint{using assumption $\;A \subseteq \color{red}{\P{A}}\;$, since $\;\subseteq\;$ is transitive $\ref 1$}
  X \subseteq \color{red}{\P{A}}
\op\equiv\hint{definition $\ref 0$ of $\;\P{\cdots}\;$}
  X \in \P{\color{red}{\P{A}}}
\endcalc$$
By the definition of $\;\subseteq\;$, this proves that $\;\P{A} \subseteq \P{\color{red}{\P{A}}}\;$.

Above I used the definition of $\;\P{\cdots}\;$ in the following form: for all $\;X\;$ and $\;A\;$ we have
$$
\tag 0
X \in \P{A} \;\equiv\; X \subseteq A
$$
And transitivity of $\;\subseteq\;$ is just
$$
\tag 1
A \subseteq B \;\land\; B \subseteq C \;\then\; A \subseteq C
$$
for all $\;A,B,C\;$.
The nice thing is that the above proof does not use the internal structure of the right hand side $\;\color{red}{\P{A}}\;$.  Therefore we can replace it with $\;\color{red}{B}\;$ throughout, resulting in a proof of the following more general theorem:
$$
\tag 2
A \subseteq \color{red}{B} \;\color{green}{\then}\; \P{A} \subseteq \P{\color{red}{B}}
$$
Finally, note that we also can prove the even stronger
$$
\tag 3
A \subseteq B \;\color{green}{\equiv}\; \P{A} \subseteq \P{B}
$$
but let me leave that as an exercise for the reader.
