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

\begin{document}
  \chapter{Ordered pairs and Cartesian products}\label{chapter:pairs-and-products}

  \filename{foundations/sections/04_pairs-and-products.ftl.tex}

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

    [readtex \path{foundations/sections/01_classes.ftl.tex}]

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


  \section{Pairs}

  \begin{forthel}
    \begin{axiom}\printlabel{FOUNDATIONS_04_8464577431863296}
      Let $a, a', b, b'$ be objects.
      Then \[ (a, b) = (a', b') \implies (\text{$a = a'$ and $b = b'$}). \]
    \end{axiom}
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_04_4782386822774784}
      A pair is an object $p$ such that $p = (a, b)$ for some objects $a, b$.
    \end{definition}

    Let an ordered pair stand for a pair.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_04_6746145623638016}
      Let $p$ be a pair.
      $\pi_{1} p$ is the object $a$ such that $p = (a, b)$ for
      some object $b$.
    \end{definition}

    Let the first entry of $p$ stand for $\pi_{1} p$.
    Let the first component of $p$ stand for the first entry of $p$.
  \end{forthel}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_04_3750179243032576}
      Let $p$ be a pair.
      $\pi_{2} p$ is the object $b$ such that $p = (a, b)$ for
      some object $a$.
    \end{definition}

    Let the second entry of $p$ stand for $\pi_{2} p$.
    Let the second component of $p$ stand for the second entry of $p$.
  \end{forthel}


  \section{Cartesian products}

  \begin{forthel}
    \begin{definition}\printlabel{FOUNDATIONS_04_2877806274936832}
      Let $A, B$ be classes.
      The Cartesian product of $A$ and $B$ is
      \[ \{ (a, b) \mid \text{$a \in A$ and $b \in B$} \}. \]
    \end{definition}

    Let the direct product of $A$ and $B$ stand for  the Cartesian product of
    $A$ and $B$.
    Let $A \times B$ stand for the Cartesian product of $A$ and $B$.
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_04_1581118511906816}
      Let $A, B$ be classes and $a, b$ be objects.
      Then \[ (a, b) \in A \times B \iff (\text{$a \in A$ and $b \in B$}). \]
    \end{proposition}
    \begin{proof}
      Case $(a, b) \in A \times B$.
        We can take $a' \in A$ and $b' \in B$ such that $(a, b) = (a', b')$.
        Then $a = a'$ and $b = b'$.
        Hence $a \in A$ and $b \in B$.
      End.

      Case $a \in A$ and $b \in B$.
        $a$ and $a$ are objects.
        Hence $(a, b)$ is an object.
        Therefore $(a, b) \in A \times B$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_04_2198552029691904}
      Let $A, B$ be classes.
      Then $A \times B$ is empty iff $A$ is empty or $B$ is empty.
    \end{proposition}
    \begin{proof}
      Case $A \times B$ is empty.
        Assume that $A$ and $B$ are nonempty.
        Then we can take an element $a$ of $A$ and an element $b$ of $B$.
        Then $(a, b) \in A \times B$.
        Contradiction.
      End.

      Case $A$ is empty or $B$ is empty.
        Assume that $A \times B$ is nonempty.
        Then we can take an element $c$ of $A \times B$.
        Then $c = (a, b)$ for some $a \in A$ and some $b \in B$.
        Hence $A$ and $B$ are nonempty.
        Contradiction.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_04_7971087096741888}
      Let $a, b$ be objects.
      Then \[ \set{a} \times \set{b} = \set{(a, b)}. \]
    \end{proposition}
    \begin{proof}
      Let us show that $\set{a} \times \set{b} \subseteq \set{(a, b)}$.
        Let $c \in \set{a} \times \set{b}$.
        Take $a' \in \set{a}$ and $b' \in \set{b}$ such that $c = (a', b')$.
        We have $a' = a$ and $b' = b$.
        Hence $c = (a, b)$.
        Thus $c \in \set{(a, b)}$.
      End.

      Let us show that $\set{(a, b)} \subseteq \set{a} \times \set{b}$.
        Let $c \in \set{(a, b)}$.
        Then $c = (a, b)$.
        We have $a \in \set{a}$ and $b \in \set{b}$.
        Hence $c \in \set{a} \times \set{b}$.
      End.
    \end{proof}
  \end{forthel}

  \begin{forthel}
    \begin{proposition}\printlabel{FOUNDATIONS_04_7456594440749056}
      Let $A, A', B, B'$ be nonempty classes.
      Then \[ A \times B = A' \times B' \implies
      (\text{$A = A'$ and $B = B'$}). \]
    \end{proposition}
    \begin{proof}
      Assume $A \times B = A' \times B'$.

      (1) $A \subseteq A'$ and $B \subseteq B'$. \\
      Proof.
        Let $a \in A$ and $b \in B$.
        Then $(a,b) \in A \times B$.
        Hence $(a,b) \in A' \times B'$.
        Thus $a \in A'$ and $b \in B'$.
      Qed.

      (2) $A' \subseteq A$ and $B' \subseteq B$. \\
      Proof.
        Let $a \in A'$ and $b \in B'$.
        Then $(a,b) \in A' \times B'$.
        Hence $(a,b) \in A \times B$.
        Thus $a \in A$ and $b \in B$.
      Qed.
    \end{proof}
  \end{forthel}
\end{document}
