\documentclass[../../set-theory/set-theory.tex]{subfiles}

\begin{document}
  \chapter{Symmetric difference}\label{chapter:symmetric-difference}

  \filename{foundations/sections/03_symmetric-difference.ftl.tex}

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{foundations/sections/02_computation-laws-for-classes.ftl.tex}]

    %[prove on][check on]
  \end{forthel}


  \section{Definitions}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_03_7457594151010304}
      Let $A, B$ be classes.
      \[ A \symdiff B = (A \cup B) \setminus (A \cap B). \]
    \end{definition}

    Let the symmetric difference of $A$ and $B$ stand for $A \symdiff B$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_4886447211413504}
      Let $A, B$ be classes.
      Then \[ A \symdiff B = (A \setminus B) \cup (B \setminus A). \]
    \end{proposition}
    \begin{proof}
      Let us show that $A \symdiff B \subseteq
      (A \setminus B) \cup (B \setminus A)$.
        Let $u \in A \symdiff B$.
        Then $u \in A \cup B$ and $u \notin A \cap B$.
        Hence ($u \in A$ or $u \in B$) and not ($u \in A$ and $u \in B$).
        Thus ($u \in A$ or $u \in B$) and ($u \notin A$ or $u \notin B$).
        Therefore if $u \in A$ then $u \notin B$.
        If $u \in B$ then $u \notin A$.
        Then we have ($u \in A$ and $u \notin B$) or
        ($u \in B$ and $u \notin A$).
        Hence $u \in A \setminus B$ or $u \in B \setminus A$.
        Thus $u \in (A \setminus B) \cup (B \setminus A)$.
      End.

      Let us show that $((A \setminus B) \cup (B \setminus A)) \subseteq
      A \symdiff B$. %!
        Let $u \in (A \setminus B) \cup (B \setminus A)$.
        Then ($u \in A$ and $u \notin B$) or ($u \in B$ and $u \notin A$).
        If $u \in A$ and $u \notin B$ then $u \in A \cup B$ and
        $u \notin A \cap B$.
        If $u \in B$ and $u \notin A$ then $u \in A \cup B$ and
        $u \notin A \cap B$.
        Hence $u \in A \cup B$ and $u \notin A \cap B$.
        Thus $u \in (A \cup B) \setminus (A \cap B) = A \symdiff B$.
      End.
    \end{proof}
  \end{forthel}


  \section{Computation laws}

  \subsection*{Commutativity}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_4518372049944576}
      Let $A, B$ be classes.
      Then \[ A \symdiff B = B \symdiff A. \]
    \end{proposition}
    \begin{proof}
      $A \symdiff B
        = (A \cup B) \setminus (A \cap B)
        = (B \cup A) \setminus (B \cap A)
        = B \symdiff A$.
    \end{proof}
  \end{forthel}


  \subsection*{Associativity}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_8680845204258816}
      Let $A, B, C$ be classes.
      Then \[ (A \symdiff B) \symdiff C = A \symdiff (B \symdiff C). \]
    \end{proposition}
    \begin{proof}
      Take a class $X$ such that $X = (((A \setminus B) \cup (B \setminus A))
      \setminus C) \cup (C \setminus ((A \setminus B) \cup (B \setminus A)))$.

      Take a class $Y$ such that $Y = (A \setminus ((B \setminus C) \cup
      (C \setminus B))) \cup (((B \setminus C) \cup (C \setminus B)) \setminus A)$.

      We have $A \symdiff B = (A \setminus B) \cup (B \setminus A)$ and
      $B \symdiff C = (B \setminus C) \cup (C \setminus B)$.
      Hence $(A \symdiff B) \symdiff C = X$ and $A \symdiff (B \symdiff C) = Y$.

      Let us show that (I) $X \subseteq Y$.
        Let $x \in X$.

        (I 1) Case $x \in ((A \setminus B) \cup (B \setminus A)) \setminus C$.
          Then $x \notin C$.

          (I 1a) Case $x \in A \setminus B$.
            Then $x \notin B \setminus C$ and $x \notin C \setminus B$.
            $x \in A$.
            Hence $x \in A \setminus ((B \setminus C) \cup (C \setminus B))$.
            Thus $x \in Y$.
          End.

          (I 1b) Case $x \in B \setminus A$.
            Then $x \in B \setminus C$.
            Hence $x \in (B \setminus C) \cup (C \setminus B)$.
            $x \notin A$.
            Thus $x \in ((B \setminus C) \cup (C \setminus B)) \setminus A$.
            Therefore $x \in Y$.
          End.
        End.

        (I 2) Case $x \in C \setminus ((A \setminus B) \cup (B \setminus A))$.
          Then $x \in C$.
          $x \notin A \setminus B$ and $x \notin B \setminus A$.
          Hence not ($x \in A \setminus B$ or $x \in B \setminus A$).
          Thus not (($x \in A$ and $x \notin B$) or ($x \in B$ and $x \notin A$)).
          Therefore ($x \notin A$ or $x \in B$) and ($x \notin B$ or $x \in A$).

          (I 2a) Case $x \in A$.
            Then $x \in B$.
            Hence $x \notin (B \setminus C) \cup (C \setminus B)$.
            Thus $x \in A \setminus ((B \setminus C) \cup (C \setminus B))$.
            Therefore $x \in Y$.
          End.

          (I 2b) Case $x \notin A$.
            Then $x \notin B$.
            Hence $x \in C \setminus B$.
            Thus $x \in (B \setminus C) \cup (C \setminus B)$.
            Therefore $x \in ((B \setminus C) \cup (C \setminus B)) \setminus A$.
            Then we have $x \in Y$.
          End.
        End.
      End.

      Let us show that (II) $Y \subseteq X$.
        Let $y \in Y$.

        (II 1) Case $y \in A \setminus ((B \setminus C) \cup (C \setminus B))$.
          Then $y \in A$.
          $y \notin B \setminus C$ and $y \notin C \setminus B$.
          Hence not ($y \in B \setminus C$ or $y \in C \setminus B$).
          Thus not (($y \in B$ and $y \notin C$) or ($y \in C$ and $y \notin B$)).
          Therefore ($y \notin B$ or $y \in C$) and ($y \notin C$ or $y \in B$).

          (II 1a) Case $y \in B$.
            Then $y \in C$.
            $y \notin A \setminus B$ and $y \notin B \setminus A$.
            Hence $y \notin (A \setminus B) \cup (B \setminus A)$.
            Thus $y \in C \setminus ((A \setminus B) \cup (B \setminus A))$.
            Therefore $y \in X$.
          End.

          (II 1b) Case $y \notin B$.
            Then $y \notin C$.
            $y \in A \setminus B$.
            Hence $y \in (A \setminus B) \cup (B \setminus A)$.
            Thus $y \in ((A \setminus B) \cup (B \setminus A)) \setminus C$.
            Therefore $y \in X$.
          End.
        End.

        (II 2) Case $y \in ((B \setminus C) \cup (C \setminus B)) \setminus A$.
          Then $y \notin A$.

          (II 2a) Case $y \in B \setminus C$.
            Then $y \in B \setminus A$.
            Hence $y \in (A \setminus B) \cup (B \setminus A)$.
            Thus $y \in ((A \setminus B) \cup (B \setminus A)) \setminus C$.
            Therefore $y \in X$.
          End.

          (II 2b) Case $y \in C \setminus B$.
            Then $y \in C$.
            $y \notin A \setminus B$ and $y \notin B \setminus A$.
            Hence $y \notin (A \setminus B) \cup (B \setminus A)$.
            Thus $y \in C \setminus ((A \setminus B) \cup (B \setminus A))$.
            Therefore $y \in X$.
          End.
        End.
      End.
    \end{proof}
  \end{forthel}


  \subsection*{Distributivity}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_4119141910839296}
      Let $A, B, C$ be classes.
      Then \[ A \cap (B \symdiff C) = (A \cap B) \symdiff (A \cap C). \]
    \end{proposition}
    \begin{proof}
      $A \cap (B \symdiff C)
        = A \cap ((B \setminus C) \cup (C \setminus B))
        = (A \cap (B \setminus C)) \cup (A \cap (C \setminus B))$.

      $A \cap (B \setminus C) = (A \cap B) \setminus (A \cap C)$.
      $A \cap (C \setminus B) = (A \cap C) \setminus (A \cap B)$.

      Hence $A \cap (B \symdiff C)
        = ((A \cap B) \setminus (A \cap C)) \cup ((A \cap C) \setminus (A \cap B))
        = (A \cap B) \symdiff (A \cap C)$.
    \end{proof}
  \end{forthel}


  \subsection*{Miscellaneous rules}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_7383417205293056}
      Let $A, B$ be classes.
      Then \[ A \subseteq B \iff A \symdiff B = B \setminus A. \]
    \end{proposition}
    \begin{proof}
      Case $A \subseteq B$.
        Then $A \cup B = B$ and $A \cap B = A$.
        Hence the thesis.
      End.

      Case $A \symdiff B = B \setminus A$.
        Let $a \in A$.
        Then $a \notin B \setminus A$.
        Hence $a \notin A \symdiff B$.
        Thus $a \notin A \cup B$ or $a \in A \cap B$.
        Indeed $A \symdiff B = (A \cup B) \setminus (A \cap B)$.
        If $a \notin A \cup B$ then we have a contradiction.
        Therefore $a \in A \cap B$.
        Then we have the thesis.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_4490230937681920}
      Let $A, B, C$ be classes.
      Then \[ A \symdiff B = A \symdiff C \iff B = C. \]
    \end{proposition}
    \begin{proof}
      Case $A \symdiff B = A \symdiff C$.

        Let us show that $B \subseteq C$.
          Let $b \in B$.

          Case $b \in A$.
            Then $b \notin A \symdiff B$.
            Hence $b \notin A \symdiff C$.
            Therefore $b \in A \cap C$.
            Indeed $A \symdiff C = (A \cup C) \setminus (A \cap C)$.
            Hence $b \in C$.
          End.

          Case $b \notin A$.
            Then $b \in A \symdiff B$.
            Indeed $b \in A \cup B$ and $b \notin A \cap B$.
            Hence $b \in A \symdiff C$.
            Thus $b \in A \cup C$ and $b \notin A \cap C$.
            Therefore $b \in A$ or $b \in C$.
            Then we have the thesis.
          End.
        End.

        Let us show that $C \subseteq B$.
          Let $c \in C$.

          Case $c \in A$.
            Then $c \notin A \symdiff C$.
            Hence $c \notin A \symdiff B$.
            Therefore $c \in A \cap B$.
            Indeed $c \notin A \cup B$ or $c \in A \cap B$.
            Hence $c \in B$.
          End.

          Case $c \notin A$.
            Then $c \in A \symdiff C$.
            Indeed $c \in A \cup C$ and $c \notin A \cap C$.
            Hence $c \in A \symdiff B$.
            Thus $c \in A \cup B$ and $c \notin A \cap B$.
            Therefore $c \in A$ or $c \in B$.
            Then we have the thesis.
          End.
        End.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_4578696040022016}
      Let $A$ be a class.
      Then \[ A \symdiff A = \emptyset. \]
    \end{proposition}
    \begin{proof}
      $A \symdiff A
        = (A \cup A) \setminus (A \cap A)
        = A \setminus A
        = \emptyset$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_6698730398941184}
      Let $A$ be a class.
      Then \[ A \symdiff \emptyset = A. \]
    \end{proposition}
    \begin{proof}
      $A \symdiff \emptyset
        = (A \cup \emptyset) \setminus (A \cap \emptyset)
        = A \setminus \emptyset
        = A$.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_03_6111806917443584}
      Let $A, B$ be classes.
      Then \[ A = B \iff A \symdiff B = \emptyset. \]
    \end{proposition}
    \begin{proof}
      Case $A = B$.
        Then $A \symdiff B
          = (A \cup A) \setminus (A \cap A)
          = A \setminus A
          = \emptyset.$
        Hence the thesis.
      End.

      Case $A \symdiff B = \emptyset$.
        Then $(A \cup B) \setminus (A \cap B)$ is empty.
        Hence every element of $A \cup B$ is an element of $A \cap B$.
        Thus for all objects $u$ if $u \in A$ or $u \in B$ then $u \in A$ and
        $u \in B$.
        Therefore every element of $A$ is an element of $B$.
        Every element of $B$ is an element of $A$.
        Then we have the thesis.
      End.
    \end{proof}
  \end{forthel}
\end{document}
