\import{set/powerset.tex}
\import{set/fixpoint.tex}
\import{function.tex}


\begin{definition}\label{equinum}
    $A$ is equinumerous with $B$ iff there exists a bijection from $A$ to $B$.
\end{definition}

\begin{abbreviation}\label{approx}
    $A\approx B$ iff $A$ is equinumerous with $B$.
\end{abbreviation}

\begin{proposition}\label{equinum_refl}
    $A\approx A$.
\end{proposition}
\begin{proof}
    $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_elem_bijections}.
    Follows by \cref{equinum}.
\end{proof}

\begin{proposition}\label{equinum_sym}
    Suppose $A\approx B$. Then $B\approx A$.
\end{proposition}
\begin{proof}
    Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}.
    Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}.
    Follows by \cref{equinum}.
\end{proof}

\begin{proposition}\label{equinum_tran}
    Suppose $A\approx B\approx C$. Then $A\approx C$.
\end{proposition}
\begin{proof}
    Take $f$ such that $f$ is a bijection from $A$ to $B$ by \cref{equinum}.
    Take $g$ such that $g$ is a bijection from $B$ to $C$ by \cref{equinum}.
    Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}.
    Follows by \cref{equinum}.
\end{proof}



\begin{theorem}[Cantor--Schröder--Bernstein]\label{cantorschroederbernstein}
    Let $f$ be an injective function from $A$ to $B$.
    Let $g$ be an injective function from $B$ to $A$.
    Then $A\approx B$.
\end{theorem}
\begin{proof}
    For all $X\in\pow{A}$ we have
        $A\setminus \img{g}{B\setminus\img{f}{X}}\subseteq A$
        by \cref{setminus_subseteq}.
    For all $X\in\pow{A}$ we have
        $A\setminus \img{g}{B\setminus\img{f}{X}}\in\pow{A}$
        by \cref{powerset_intro}.
    Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$.
    For all $X\in\pow{A}$ we have
        $(X,A\setminus \img{g}{B\setminus\img{f}{X}})\in h$ by assumption.
    $h$ is a relation by \cref{relation}.
    $h$ is right-unique by \cref{rightunique,pair_eq_iff}.
    Thus $h$ is a function by assumption.
    For all $X\in\pow{A}$ we have
        $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$
        by \cref{function_apply_intro}.
    For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by assumption.
    For all $X$ we have if $X\in\dom{h}$, then $X\in\pow{A}$
        by \cref{dom_iff,pair_eq_iff}.
    For all $X$ we have if $X\in\pow{A}$, then $X\in\dom{h}$
        by \cref{dom_iff}.
    Thus $\dom{h} = \pow{A}$ by set extensionality.
    $h$ is a function to $\pow{A}$ by assumption.
    Thus $h$ is a function from $\pow{A}$ to $\pow{A}$ by \cref{funs_intro}.

    $h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating).

    Take $X$ such that $X$ is a fixpoint of $h$ by \cref{knastertarski}.
    Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}.

    $\img{g}{B\setminus\img{f}{X}}\subseteq A$.

    Thus $\img{g}{B\setminus\img{f}{X}} = A\setminus X$ by \cref{double_relative_complement}.

    Let $h' = \restrl{h}{X}$.

    Omitted. % TODO
\end{proof}