Theorem: Bijection between Power Set of Disjoint Union and Cartesian Product of Power Sets

Let $S$ and $T$ be disjoint sets.
Let $\powerset S$ denote the power set of $S$.
Then there exists a bijection between $\powerset {S \cup T}$ and $\paren {\powerset S} \times \paren {\powerset T}$.
Hence:
:$\powerset {S \cup T} \sim \paren {\powerset S} \times \paren {\powerset T}$
where $\sim$ denotes set equivalence.

Proof:
Let $\phi: \paren {\powerset S} \times \paren {\powerset T} \to  \powerset {S \cup T}$ be defined as:
:$\forall \tuple {A, B} \in \paren {\powerset S} \times \paren {\powerset T}: \map \phi {A, B} = A \cup B$
In order to show that $\phi$ is a bijection, it needs to be shown that $\phi$ has the following properties:
:$\phi$ is a mapping, that is:
::$\phi$ is left-total
::$\phi$ is many-to-one
:$\phi$ is a surjection
:$\phi$ is an injection.
Let $A \subseteq S$ and $B \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = A
      | o = \in
      | r = \powerset S
      | c = {{Defof|Power Set}}
}}
{{eqn | lo= \land
      | l = B
      | o = \in
      | r = \powerset T
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {A, B}
      | o = \in
      | r = \paren {\powerset S} \times \paren {\powerset T}
      | c = {{Defof|Cartesian Product}}
}}
{{end-eqn}}
Thus:
:$\forall A \subseteq S, B \subseteq T: \tuple {A, B} \in \Dom \phi$
and so $\phi$ is left-total.
{{qed|lemma}}
Let $A_1, A_2 \subseteq S$ and $B_1, B_2 \subseteq T$.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi {A_1, B_1}
      | o = \ne
      | r = \map \phi {A_2, B_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_1 \cup B_1
      | o = \ne
      | r = A_2 \cup B_2
      | c = Definition of $\phi$
}}
{{eqn | ll= \leadsto
      | l = A_1 \cup B_1
      | o = \nsubseteq
      | r = A_2 \cup B_2
      | c = {{Defof|Set Equality}}
}}
{{eqn | lo= \lor
      | l = A_2 \cup B_2
      | o = \nsubseteq
      | r = A_1 \cup B_1
      | c = 
}}
{{end-eqn}}
{{WLOG}}, suppose $A_1 \cup B_1 \nsubseteq A_2 \cup B_2$.
Then:
{{begin-eqn}}
{{eqn | q = \exists x \in A_1 \cup B_1
      | l = x
      | o = \notin
      | r = A_2 \cup B_2
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in A_1 \lor x \in B_1
      | l = x \notin A_2
      | o = \land
      | r = x \notin B_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_1 \ne A_2
      | o = \lor
      | r = A_1 \ne B_2
      | c = 
}}
{{eqn | lo= \land
      | l = B_1 \ne A_2
      | o = \lor
      | r = B_1 \ne B_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {A_1, B_1}
      | o = \ne
      | r = \tuple {A_2, B_2}
      | c = 
}}
{{end-eqn}}
That is:
:$\map \phi {A_1, B_1} \ne \map \phi {A_2, B_2} \implies \tuple {A_1, B_1} \ne \tuple {A_2, B_2}$
demonstrating that $\phi$ is many-to-one.
Thus $\phi$ has been shown to be a mapping.
{{qed|lemma}}
Let $A \cup B \in \powerset {S \cup T}$.
Then:
:$\tuple {A, B} \in \paren {\powerset S} \times \paren {\powerset T}$
by definition of power set and Cartesian product.
That is, $\phi$ is a surjection by definition.
{{qed|lemma}}
It remains to be shown that $\phi$ is an injection.
Let $\tuple {A_1, B_1} \ne \tuple {A_2, B_2}$.
Then either $A_1 \ne A_2$ or $B_1 \ne B_2$.
That is, at least one of the following holds:
{{begin-eqn}}
{{eqn | l = A_1
      | o = \nsubseteq
      | r = A_2
}}
{{eqn | l = A_2
      | o = \nsubseteq
      | r = A_1
}}
{{eqn | l = B_1
      | o = \nsubseteq
      | r = B_2
}}
{{eqn | l = B_2
      | o = \nsubseteq
      | r = B_1
}}
{{end-eqn}}
{{WLOG}}, suppose $A_1 \nsubseteq A_2$.
Then:
:$\exists x \in A_1: x \notin A_2$
and so by Set is Subset of Union:
:$x \in A_1 \cup B_1$
But we have that $S$ and $T$ are disjoint.
That is:
:$x \in A_1 \implies x \notin B_2$
Thus:
:$\exists x \in A_1 \cup B_1: x \notin A_2 \cup B_2$
and so:
:$A_1 \cup B_1 \ne A_2 \cup B_2$
That is:
:$\map \phi {A_1, B_1} \ne \map \phi {A_2, B_2}$
demonstrating that $\phi$ is an injection.
Hence the result.
{{qed}}