# 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$
:::