---
# System prepended metadata

title: Simpler Proof of Zorn's Lemma
tags: [Set Theory]

---

# Simpler Proof of Zorn's Lemma

###### tags: `Set Theory`


## Definitions

:::success
* $P(A, x) \equiv \{u \in A \mid u < x\}$

* Totally ordered sets
    $\mathrm{TO}(X, \leq) \equiv \{A \subseteq X \mid \forall x, y \in A \colon x \leq y \lor y \leq x\}$

* Conforming sets
    $\mathrm{CONF}(X, f) \equiv \left\{ A \in \mathrm{TO}(X, \leq) \,\middle|\, \begin{array}{l} \forall S \subseteq A \colon \bigl( S \neq \varnothing \implies \exists x \in S, \forall u \in S \colon x \leq u \bigr) \\ \forall x \in A \colon x = f(P(A, x)) \end{array} \right\}$
:::


## Axiom of Choice

:::success
$\exists f \in \mathrm{TO}(X, \leq) \to X, \forall A \in \mathrm{TO}(X, \leq) \colon \\
    \bigl( \forall u \in A \colon u < f(A) \bigr) \lor \bigl( \forall u \in A \colon u \leq f(A) \bigr) \land \bigl( \forall u \in X \colon f(A) \not< u \bigr)$
:::

:::info
$\forall A \in \mathrm{TO}(X, \leq), u \in A \colon u \leq f(A)$
:::

:::warning
* $\forall A \in \mathrm{TO}(X, \leq)$
    * $\bigl( \forall u \in A \colon u < f(A) \bigr) \lor \bigl( \forall u \in A \colon u \leq f(A) \bigr) \land \bigl( \forall u \in X \colon f(A) \not< u \bigr)$
    * $\bigl( \forall u \in A \colon u < f(A) \bigr) \lor \bigl( \forall u \in A \colon u \leq f(A) \bigr)$
    * $\forall u \in A$
        * $u < f(A) \lor u \leq f(A)$
        * $u \leq f(A)$
:::


## Properties

:::info
$\forall A \in \mathrm{CONF}(X, f), \forall S \colon \Bigl( A \setminus S \neq \varnothing \implies \exists x \in A \setminus S \colon \bigl( \forall u \in A \setminus S \colon x \leq u \bigr) \land P(A, x) \subseteq S \Bigr)$
:::

:::warning
* $\forall A \in \mathrm{CONF}(X, f), \forall S$
    * $(1) \colon \because A \in \mathrm{CONF}(X, f) \land A \setminus S \neq \varnothing \therefore \exists x \in A, \forall u \in A \setminus S \colon x \leq u$
    * $(2) \colon \forall y \in P(A, x)$
        * $y \in A \land y < x$
        * $\because \bigl( \forall u \in A \setminus S \colon x \leq u \bigr) \land y < x \therefore y \notin A \setminus S$
        * $(*) \colon \because y \in A \land y \notin A \setminus S \therefore y \in S$
    * $\because (1) \land (2 \colon *) \therefore \exists x \in A \setminus S \colon \bigl( \forall u \in A \setminus S \colon x \leq u \bigr) \land P(A, x) \subseteq S$
:::

:::info
$\forall A \in \mathrm{CONF}(X, f), \forall S \colon \Bigl( \forall x \in A \colon \bigl( P(A, x) \subseteq S \implies x \in S \bigr) \implies A \subseteq S \Bigr)$
:::

:::warning
* $\forall A \in \mathrm{CONF}(X, f), \forall S \colon \Bigl( \forall x \in A \colon \bigl( P(A, x) \subseteq S \implies x \in S \bigr) \implies \Bigr)$
    * $\forall x \in A$
        * $P(A, x) \subseteq S \implies x \in S$
        * $\lnot \bigl( P(A, x) \subseteq S \land x \notin S \bigr)$
    * $\lnot \bigl( \exists x \in A \colon x \notin S \land P(A, x) \subseteq S \bigr)$
    * $\lnot \Bigl( \exists x \in A \setminus S, \forall u \in A \colon \bigl( u < x \implies u \in S \bigr) \Bigr)$
    * $\lnot \Bigl( \exists x \in A \setminus S, \forall u \in A \colon \bigl( u \notin S \implies u \not< x \bigr) \Bigr)$
    * $\lnot \bigl( \exists x \in A \setminus S, \forall u \in A \setminus S \colon x \leq u \bigr)$
    * $A \setminus S = \varnothing$
    * $A \subseteq S$
:::

:::info
$\forall A, B \in \mathrm{CONF}(X, f), x \in A \setminus B \colon B \subseteq P(A, x)$
:::

:::warning
* $\forall A, B \in \mathrm{CONF}(X, f), x \in A \setminus B$
    * Let $S = \bigl\{ u \in A \bigm| \forall v \in A \setminus B \colon u < v \bigr\}$
    * $\forall u \in S$
        * $u \in A \land \bigl( \forall v \in A \setminus B \colon u < v \bigr)$
        * $\because \bigl( \forall v \in A \setminus B \colon u < v \bigr) \land x \in A \setminus B \therefore u < x$
        * $\forall x \in A \land u \in A \land u < x \therefore u \in P(A, x)$
    * $S \subseteq P(A, x)$
    * $\forall y \in B \colon \bigl( P(B, y) \subseteq S \implies \bigr)$
        * $\because P(B, y) \subseteq B \therefore A \setminus P(B, y) \supseteq A \setminus B$
        * $\because x \in A \setminus B \subseteq A \setminus P(B, y) \therefore A \setminus P(B, y) \neq \varnothing$
        * $\because A \in \mathrm{CONF}(X, f) \land A \setminus P(B, y) \neq \varnothing \\
            \therefore \exists z \in A \setminus P(B, y) \colon \bigl( \forall u \in A \setminus P(B, y) \colon z \leq u \bigr) \land P(A, z) \subseteq P(B, y)$
        * $\because z \notin P(B, y) \therefore z \notin B \lor z \in B \land y \leq z$
        * $\because \bigl( z \notin B \lor z \in B \land y \leq z \bigr) \land z \in A \therefore z \in A \setminus B \lor y \leq z$
        * $\forall u \in P(B, y)$
            * $\because u \in P(B, y) \subseteq S \therefore u \in A \land \bigl( \forall v \in A \setminus B \colon u < v \bigr)$
            * $\because \bigl( z \in A \setminus B \lor y \leq z \bigr) \land \bigl( \forall v \in A \setminus B \colon u < v \bigr) \land u < y \therefore u < z \lor u < y \leq z$
            * $\because z \in A \land u \in A \land u < z \therefore u \in P(A, z)$
        * $\because P(A, z) \subseteq P(B, y) \land \bigl( \forall u \in P(B, y) \colon u \in P(A, z) \bigr) \therefore P(B, y) = P(A, z)$
        * $y = f(P(B, y)) = f(P(A, z)) = z$
        * $\forall v \in A \setminus B$
            * $\because \bigl( \forall u \in A \setminus P(B, y) \colon z \leq u \bigr) \land v \in A \setminus B \subseteq A \setminus P(B, y) \therefore y = z \leq v$
            * $\because y \in B \land v \notin B \therefore y \neq v$
            * $\because y \leq v \land y \neq v \therefore y < v$
        * $\because y = z \in A \land \bigl( \forall v \in A \setminus B \colon y < v \bigr) \therefore y \in S$
    * $\because B \in \mathrm{CONF}(X, f) \land \Bigl( \forall y \in B \colon \bigl( P(B, y) \subseteq S \implies y \in S \bigr) \Bigr) \therefore B \subseteq S$
    * $B \subseteq S \subseteq P(A, x)$
:::

:::info
$\forall A, B \in \mathrm{CONF}(X, f) \colon \Bigl( A \setminus B \neq \varnothing \implies f(B) \in A \land \bigl( \forall u \in A \setminus B \colon f(B) \leq u \bigr) \Bigr)$
:::

:::warning
* $\forall A, B \in \mathrm{CONF}(X, f) \colon \bigl( A \setminus B \neq \varnothing \implies \bigr)$
    * $\because A \in \mathrm{CONF}(X, f) \land A \setminus B \neq \varnothing \therefore \exists x \in A \setminus B \colon \bigl( \forall u \in A \setminus B \colon x \leq u \bigr) \land P(A, x) \subseteq B$
    * $\because A, B \in \mathrm{CONF}(X, f) \land x \in A \setminus B \therefore B \subseteq P(A, x)$
    * $\because P(A, x) \subseteq B \land B \subseteq P(A, x) \therefore P(A, x) = B$
    * $x = f(P(A, x)) = f(B)$
    * $\because x \in A \land \bigl( \forall u \in A \setminus B \colon x \leq u \bigr) \land x = f(B) \therefore f(B) \in A \land \bigl( \forall u \in A \setminus B \colon f(B) \leq u \bigr)$
:::

:::info
$\forall A, B \in \mathrm{CONF}(X, f) \colon A \subseteq B \lor B \subseteq A$
:::

:::warning
* $\forall A, B \in \mathrm{CONF}(X, f)$
    * $A = B \lor B \setminus A \neq \varnothing \lor A \setminus B \neq \varnothing$
    * $B \setminus A \neq \varnothing \implies$
        * $\exists x \colon x \in B \setminus A$
        * $\because A, B \in \mathrm{CONF}(X, f) \land x \in B \setminus A \therefore A \subseteq P(B, x) \subset B$
    * $A \setminus B \neq \varnothing \implies$
        * $\exists x \colon x \in A \setminus B$
        * $\because A, B \in \mathrm{CONF}(X, f) \land x \in A \setminus B \therefore B \subseteq P(A, x) \subset A$
    * $A = B \lor A \subset B \lor B \subset A$
    * $A \subseteq B \lor B \subseteq A$
:::

:::info
$\forall A, B \in \mathrm{CONF}(X, f) \colon A \cup B \in \mathrm{CONF}(X, f)$
:::

:::warning
* $\forall A, B \in \mathrm{CONF}(X, f)$
    * $B \subseteq A \lor A \subseteq B$
    * $A \cup B = A \in \mathrm{CONF}(X, f) \lor A \cup B = B \in \mathrm{CONF}(X, f)$
    * $A \cup B \in \mathrm{CONF}(X, f)$
:::


## Proof

:::info
$\forall A \in \mathrm{CONF}(X, f) \colon A \cup \{f(A)\} \in \mathrm{CONF}(X, f)$
:::

:::success
* $\forall A \in \mathrm{CONF}(X, f)$
    * $A \cup \{f(A)\} \in \mathrm{TO}(X, \leq)$
        :::warning
        * $\forall x, y \in A \cup \{f(A)\}$
            * $x, y \in A \implies x \leq y \lor y \leq x$
            * $x, y \in \{f(A)\} \implies x = y = f(A)$
            * $x \in A \land y \in \{f(A)\} \implies x \leq f(A) = y$
            * $x \in \{f(A)\} \land y \in A \implies y \leq f(A) = x$
            * $x \leq y \lor y \leq x$
        :::

    * $\forall S \subseteq A \cup \{f(A)\} \colon \bigl( S \neq \varnothing \implies \exists x \in S, \forall u \in S \colon x \leq u \bigr)$
        :::warning
        * $\forall S \subseteq A \cup \{f(A)\} \colon \bigl( S \neq \varnothing \implies \bigr)$
            * $S = S \cap \bigl( A \cup \{f(A)\} \bigr) = S \cap A \cup S \cap \{f(A)\} \subseteq S \cap A \cup \{f(A)\}$
            * $S \cap A = \varnothing \implies$
                * $S \subseteq \{f(A)\}$
                * $\because S \neq \varnothing \therefore f(A) \in S$
                * $\exists x \colon x = f(A) \in S$
                * $\forall u \in S \subseteq \{f(A)\} = \{x\} \colon x = u \leq u$
            * $S \cap A \neq \varnothing \implies$
                * $\exists x \in S \cap A, \forall u \in S \cap A \colon x \leq u$
                * $\forall u \in S \subseteq S \cap A \cup \{f(A)\}$
                    * $u \in S \cap A \lor u = f(A)$
                    * $x \leq u \lor x \leq f(A) = u$
                    * $x \leq u$
            * $\exists x \in S, \forall u \in S \colon x \leq u$
        :::

    * $\forall x \in A \cup \{f(A)\} \colon f \Bigl( P \bigl( A \cup \{f(A)\}, x \bigr) \Bigr) = x$
        :::warning
        * $\forall x \in A \cup \{f(A)\}$
            * $x \in A \lor x = f(A)$
            * $x \leq f(A) \lor x = f(A)$
            * $x \leq f(A)$
            * $\forall u \in P \bigl( A \cup \{f(A)\}, x \bigr)$
                * $\because u \in A \cup \{f(A)\} \therefore u \in A \lor u = f(A)$
                * $u \in A \lor x \leq f(A) = u$
                * $\because u < x \therefore u \in A$
            * $P \bigl( A \cup \{f(A)\}, x \bigr) \subseteq A$
            * $x \in A \implies$
                * $\forall u \in P \bigl( A \cup \{f(A)\}, x \bigr)$
                    * $u \in A$
                    * $\because x \in A \land u \in A \land u < x \therefore u \in P(A, x)$
                * $\forall u \in P(A, x)$
                    * $u \in A$
                    * $\because x \in A \cup \{f(A)\} \land u \in A \subseteq A \cup \{f(A)\} \land u < x \therefore u \in P \bigl( A \cup \{f(A)\}, x \bigr)$
                * $P \bigl( A \cup \{f(A)\}, x \bigr) = P(A, x)$
                * $f \Bigl( P \bigl( A \cup \{f(A)\}, x \bigr) \Bigr) = f(P(A, x)) = x$
            * $x \notin A \implies$
                * $\because x \in A \cup \{f(A)\} \therefore x = f(A)$
                * $\forall u \in A$
                    * $u \leq f(A) = x$
                    * $\because u \in A \land x \notin A \therefore u \neq x$
                    * $\because u \leq x \land u \neq x \therefore u < x$
                    * $\because x \in A \cup \{f(A)\} \land u \in A \subseteq A \cup \{f(A)\} \land u < x \therefore u \in P \bigl( A \cup \{f(A)\}, x \bigr)$
                * $\because P \bigl( A \cup \{f(A)\} \bigr) \subseteq A \land \Bigl( \forall u \in A \colon u \in P \bigl( A \cup \{f(A)\}, x \bigr) \Bigr) \therefore P \bigl( A \cup \{f(A)\}, x \bigr) = A$
                * $f \Bigl( P \bigl( A \cup \{f(A)\}, x \bigr) \Bigr) = f(A) = x$
            * $f \Bigl( P \bigl( A \cup \{f(A)\}, x \bigr) \Bigr) = x$
        :::
:::

:::info
$\forall \mathscr D \subseteq \mathrm{CONF}(X, f) \colon \bigcup \mathscr D \in \mathrm{CONF}(X, f)$
:::

:::success
* $\forall \mathscr D \subseteq \mathrm{CONF}(X, f)$
    * $\bigcup \mathscr D \in \mathrm{TO}(X, \leq)$
        :::warning
        * $\forall x, y \in \bigcup \mathscr D$
            * $\exists A, B \in \mathscr D \subseteq \mathrm{CONF}(X, f) \colon x \in A \land y \in B$
            * $x, y \in A \cup B \in \mathrm{CONF}(X, f) \subseteq \mathrm{TO}(X, \leq)$
            * $x \leq y \lor y \leq x$
        :::

    * $\forall S \subseteq \bigcup \mathscr D \colon \bigl( S \neq \varnothing \implies \exists x \in S, \forall u \in S \colon x \leq u \bigr)$
        :::warning
        * $\forall S \subseteq \bigcup \mathscr D \colon \bigl( S \neq \varnothing \implies \bigr)$
            * $\exists w \colon w \in S \subseteq \bigcup \mathscr D$
            * $\exists A \in \mathscr D \subseteq \mathrm{CONF}(X, f) \colon w \in A$
            * $S \cap A \neq \varnothing$
            * $\exists x \in S \cap A, \forall u \in S \cap A \colon x \leq u$
            * $\forall u \in S \subseteq \bigcup \mathscr D$
                * $\exists B \in \mathscr D \subseteq \mathrm{CONF}(X, f) \colon u \in B$
                * $u \in A \implies$
                    * $\because u \in S \cap A \therefore x \leq u$
                * $u \notin A \implies$
                    * $\because B \in \mathrm{CONF}(X, f) \land u \in B \setminus A \therefore A \subseteq P(B, u)$
                    * $\because x \in A \subseteq P(B, u) \therefore x < u$
                * $x \leq u$
            * $\exists x \in S \cap A \subseteq S, \forall u \in S \colon x \leq u$
        :::

    * $\forall x \in \bigcup \mathscr D, f \bigl( P \!\left( \bigcup \mathscr D, x \right) \bigr) = x$
        :::warning
        * $\forall x \in \bigcup \mathscr D$
            * $\exists A \in \mathscr D \subseteq \mathrm{CONF}(X, f) \colon x \in A$
            * $\forall u \in P \!\left( \bigcup \mathscr D, x \right)$
                * $\exists B \in \mathscr D \subseteq \mathrm{CONF}(X, f) \colon u \in B$
                * $\because u \in P \!\left( \bigcup \mathscr D, x \right) \therefore u < x$
                * $\because u \in B \land u < x \therefore x \notin P(B, u)$
                * $\because x \in A \land x \notin P(B, u) \therefore A \not\subseteq P(B, u)$
                * $\because A, B \in \mathrm{CONF}(X, f) \land u \in B \land A \not\subseteq P(B, u) \therefore u \in A$
                * $\because x \in A \land u \in A \land u < x \therefore u \in P(A, x)$
            * $\forall u \in P(A, x)$
                * $u \in A \land u < x$
                * $\because x \in \bigcup \mathscr D \land u \in A \subseteq \bigcup \mathscr D \land u < x \therefore u \in P \!\left( \bigcup \mathscr D, x \right)$
            * $P \!\left( \bigcup \mathscr D, x \right) = P(A, x)$
            * $f \bigl( P \!\left( \bigcup \mathscr D, x \right) \bigr) = f(P(A, x)) = x$
        :::
:::

:::info
$\forall u \in X \colon f \bigl( \bigcup \mathrm{CONF}(X, f) \bigr) \not< u$
:::

:::warning
* Let $U = \bigcup \mathrm{CONF}(X, f)$
* $U \in \mathrm{CONF}(X, f)$
* $U \cup \{f(U)\} \in \mathrm{CONF}(X, f)$
* $U \cup \{f(U)\} \subseteq \bigcup \mathrm{CONF}(X, f) = U$
* $f(U) \in U$
* $\because U \in \mathrm{CONF}(X, f) \subseteq \mathrm{TO}(X) \therefore \bigl( \forall u \in U \colon u < f(U) \bigr) \lor \bigl( \forall u \in U \colon u \leq f(U) \bigr) \land \bigl( \forall u \in X \colon f(U) \not< u \bigr)$
* $\bigl( \forall u \in U \colon u < f(U) \bigr) \lor \bigl( \forall u \in X \colon f(U) \not< u \bigr)$
* $\because f(U) \in U \therefore \lnot \bigl( \forall u \in U \colon u < f(U) \bigr)$
* $\forall u \in X \colon f(U) \not< u$
:::


## Properties of $f(\varnothing)$

:::info
* $\varnothing \in \mathrm{CONF}(X, f)$
* $\{f(\varnothing)\} \in \mathrm{CONF}(X, f)$
* $\forall A \in \mathrm{CONF}(X, f) \colon \Bigl( A \neq \varnothing \implies f(\varnothing) \in A \land \bigl( \forall u \in A \colon f(\varnothing) \leq u \bigr) \Bigr)$
:::

:::warning
* $\forall A \in \mathrm{CONF}(X, f) \colon (A \neq \varnothing \implies)$
    * $\exists x \in A, \forall u \in A \colon x \leq u$
    * $P(A, x) = \varnothing$
    * $f(\varnothing) = f(P(A, x)) = x \in A$
    * $\because f(\varnothing) = x \therefore \forall u \in A \colon f(\varnothing) \leq u$
:::
