Theorem: Set Equation: Union

Let $A$ and $B$ be sets.
Consider the set equation:
:$A \cup X = B$
The solution set of this is given by:
:$X = \begin {cases} \O & : A \nsubseteq B \\ \set {\paren {B \setminus A} \cup Y: Y \subseteq A} & : \text {otherwise} \end {cases}$

Proof:
In the first case $A$ is a not a subset of $B$.
So there exists an $x \in A$ such that $x \notin B$.
By the definition of union:
:$\forall x: x \in A \implies x \in A \cup X$
Hence the solution set is empty.
In the second case, suppose $A$ is a subset of $B$.
{{WIP}}
In particular, suppose $A$ is a subset of $B$, and $B$ is the  empty set.
By Subset of Empty Set:
:$A = \O$.
Then, {{hypothesis}}:
{{begin-eqn}}
{{eqn | l = A \cup X 
      | r = B
      | c = {{hypothesis}}
}}
{{eqn |ll = \leadsto
      | l = \O \cup X 
      | r = \O
      | c = {{hypothesis}} and result shown above
}}
{{eqn |ll = \leadsto
      | l = X 
      | r = \O
      | c = Union of Empty Set
}}
{{end-eqn}}
Hence, by Empty Set is Subset of All Sets:
:$X = \O \in \set {\paren {B \setminus A} \cup Y: Y \subseteq A}$
as required.
Suppose $A$ is a subset of $B$ and $B$ is non-empty.
By definition of a subset:
:$A \subseteq B \iff \forall x: \paren {x \in A \implies x \in B}$
Then, {{hypothesis}} and the {{axiom-link|Extension|Sets}}:
:$\forall x: \paren {x \in A \cup X \iff x \in B }$
It follows that:
:$\forall x: x \notin B \implies \neg {\paren {\paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} } }$
By Proof by Contraposition:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies x \in B$
Then:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies x \in \paren{\paren{B \cup A } \setminus A }$
By Set is Subset of Itself and the definition of existential quantifier:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists A \subseteq A: x \in \paren{\paren{B \cup A } \setminus A }$
Then, let $Y \subseteq A$ be arbitrary, such that:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: x \in \paren{\paren{B \cup Y } \setminus A }$
By definition of  set union:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{x \in Y \setminus A } \lor \paren{x \in B \setminus A }$
By Set is Subset of Union:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{x \in Y \setminus A } \lor \paren{x \in Y } \lor \paren{x \in B \setminus A }$
By Union is Commutative:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{x \in Y \setminus A } \lor \paren{x \in B \setminus A } \lor \paren{x \in Y }$
By definition of set complement:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{\paren{\paren {x \in Y } \land \paren{x \notin A } } \lor \paren{x \in B  \land x \notin A } \lor \paren{x \in Y } }$
By Double Negation/Double Negation Elimination/Proof Rule:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{\neg \paren{\neg \paren{\paren {x \in Y } \land \paren{x \notin A } } } \lor \paren{x \in B  \land x \notin A } \lor \paren{x \in Y } }$
By definition of  implication:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{\neg \paren{\paren {x \in Y } \land \paren{x \notin A } } \implies \paren{x \in B  \land x \notin A } \lor \paren{x \in Y } }$
By  De Morgan's Laws for Set Complement of Intersection:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{ \neg \paren{\paren {x \in Y } \lor \paren{x \in A } } \implies \paren{x \in B  \land x \notin A } \lor \paren{x \in Y } }$
By definition of set complement:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{ \neg \paren{\paren {x \in Y } \lor \paren{x \in A } } \implies \paren{x \in B  \setminus A } \lor \paren{x \in Y } }$
By definition of  implication:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{\paren{x \in Y \implies x \in A} \implies \paren{x \in B  \setminus A } \lor \paren{x \in Y } }$
By definition of set union:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{\paren{x \in Y \implies x \in A} \implies x \in \set{ \paren{ B \setminus A } \cup Y } }$
By definition of subset:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies \exists Y \subseteq A: \paren{ x \in Y \implies x \in \set{ \paren{ B \setminus A } \cup Y } }$
By definition of set-builder notation:
:$\forall x: \paren {x \in A \implies x \in B} \land \paren {x \in A \cup X \iff x \in B} \implies x \in \set {\paren{B \setminus A} \cup Y :Y \subseteq A }$
Hence:
:$\forall X: A \subseteq B \land \paren {A \cup X = B} \implies X = \set {\paren {B \setminus A} \cup Y :Y \subseteq A }$
as required.
{{qed|lemma}}
{{proof wanted|formalising the second case}}
Category:Set Theory
Category:Set Union
3o7m6qiwk0sx5t3kf8vjw6zqs58iszy