diff options
Diffstat (limited to 'library/ordinal.tex')
| -rw-r--r-- | library/ordinal.tex | 262 |
1 files changed, 188 insertions, 74 deletions
diff --git a/library/ordinal.tex b/library/ordinal.tex index f978257..f7a66d1 100644 --- a/library/ordinal.tex +++ b/library/ordinal.tex @@ -19,7 +19,7 @@ so we will explicitly talk about \emph{\in-transitivity} here. % \renewcommand{\in}{\ensuremath{\mathonlyin}} % \begin{definition}\label{transitiveset} - A set $A$ is \in-transitive iff for all $x, y$ + $A$ is \in-transitive iff for all $x, y$ such that $x\in y\in A$ we have $x\in A$. \end{definition} @@ -27,12 +27,16 @@ so we will explicitly talk about \emph{\in-transitivity} here. $A$ is \in-transitive iff for all $a\in A$ we have $a\subseteq A$. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,subseteq}. +\end{proof} \begin{proposition}\label{transitiveset_iff_pow} $A$ is \in-transitive iff $A\subseteq \pow{A}$. \end{proposition} \begin{proof} - For all $a\in A$ we have $a\subseteq A \iff a\in\pow{A}$. + For all $a\in A$ we have $a\subseteq A \iff a\in\pow{A}$ + by \cref{subseteq,pow_iff}. Follows by \cref{elem_subseteq,subseteq,pow_iff,transitiveset_iff_subseteq}. \end{proof} @@ -40,18 +44,28 @@ so we will explicitly talk about \emph{\in-transitivity} here. $A$ is \in-transitive iff $\unions{\suc{A}} = A$. \end{proposition} \begin{proof} - Follows by \cref{transitiveset,subseteq,subseteq_antisymmetric,suc,transitiveset_iff_pow,unions_subseteq_of_powerset_is_subseteq,unions_iff,suc_subseteq_intro,powerset_top}. + We have if $A$ is \in-transitive, then $\unions{\suc{A}}=A$ + by \cref{setext,transitiveset,unions_iff,suc_iff}. + We have if $\unions{\suc{A}}=A$, then $A$ is \in-transitive + by \cref{transitiveset,unions_iff,suc_iff}. + Follows by assumption. \end{proof} \begin{proposition}\label{transitiveset_iff_unions_subseteq} $A$ is \in-transitive iff $\unions{A}\subseteq A$. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,subseteq,unions_iff}. +\end{proof} \begin{proposition}\label{transitiveset_upair} Suppose $A$ is \in-transitive. Suppose $\{a,b\}\in A$. Then $a,b\in A$. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,transitiveset_iff_subseteq,subseteq}. +\end{proof} % For Kuratowski pairs only: %\begin{proposition}\label{transitiveset_pair} @@ -81,26 +95,41 @@ so we will explicitly talk about \emph{\in-transitivity} here. \begin{proposition}\label{emptyset_transitiveset} $\emptyset$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,emptyset}. +\end{proof} \begin{proposition}\label{union_of_transitiveset_is_transitiveset} Suppose $A$ and $B$ are \in-transitive. Then $A\union B$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,union_iff}. +\end{proof} \begin{proposition}\label{inter_of_transitiveset_is_transitiveset} Let $A, B$ be \in-transitive sets. Then $A\inter B$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,inter}. +\end{proof} \begin{proposition}\label{suc_of_transitiveset_is_transitiveset} Let $A$ be an \in-transitive set. Then $\suc{A}$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,suc}. +\end{proof} \begin{proposition}\label{unions_of_transitiveset_is_transitiveset} Let $A$ be an \in-transitive set. Then $\unions{A}$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{transitiveset,unions_iff}. +\end{proof} \begin{proposition}\label{unions_family_of_transitiveset_is_transitiveset} Suppose every element of $A$ is an \in-transitive set. @@ -132,28 +161,43 @@ so we will explicitly talk about \emph{\in-transitivity} here. Suppose every element of $\alpha$ is \in-transitive. Then $\alpha$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} \begin{proposition}\label{ordinal_is_transitiveset} Let $\alpha$ be an ordinal. Then $\alpha$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} \begin{proposition}\label{ordinal_elem_is_transitiveset} Let $\alpha$ be an ordinal. Suppose $A\in\alpha$. Then $A$ is \in-transitive. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} \begin{proposition}\label{elem_of_ordinal_is_ordinal} Let $\alpha$ be an ordinal. Suppose $\beta\in\alpha$. Then $\beta$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset}. +\end{proof} \begin{proposition}\label{suc_ordinal_implies_ordinal} Suppose $\suc{\alpha}$ is an ordinal. Then $\alpha$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,suc}. +\end{proof} \begin{proposition}\label{transitivesubseteq_of_ordinal_is_ordinal} Let $\alpha$ be an ordinal. @@ -170,6 +214,9 @@ so we will explicitly talk about \emph{\in-transitivity} here. Suppose $\alpha\in\beta$. Then $\alpha\subseteq\beta$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset_iff_subseteq}. +\end{proof} \begin{proposition}\label{ordinal_transitivity} Let $\alpha$ be an ordinal. @@ -186,6 +233,9 @@ so we will explicitly talk about \emph{\in-transitivity} here. Suppose $\alpha\in\beta$. Then $\suc{\alpha}\subseteq\beta$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset_iff_subseteq,suc_subseteq_intro}. +\end{proof} \begin{abbreviation}\label{ordinal_prec} @@ -217,26 +267,42 @@ We already have global irreflexivity and asymmetry of \in. \in\ is transitive on ordinals by definition. To show that \in\ is a strict total order it only remains to show that \in\ is connex. +\begin{lemma}\label{ordinal_elem_connex_from_elements} + Let $\alpha,\gamma$ be ordinals. + Suppose for all sets $\xi,\beta$ such that $\xi\in\alpha$ and $\beta$ is an ordinal + we have $\xi\in\beta\lor \beta\in\xi \lor \xi = \beta$. + Suppose for every $\eta\in\gamma$ + we have $\alpha\in\eta\lor \eta\in\alpha \lor \alpha = \eta$. + Then $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. +\end{lemma} +\begin{proof} + Assume neither $\alpha\in\gamma$ nor $\gamma\in\alpha$. + For every $\xi\in\alpha$ we have $\xi\in\gamma$ + by \cref{ordinal_transitivity}. + Thus $\alpha\subseteq\gamma$ by \cref{subseteq}. + For every $\eta\in\gamma$ we have $\eta\in\alpha$ + by \cref{ordinal_transitivity}. + Thus $\gamma\subseteq\alpha$ by \cref{subseteq}. + Follows by \cref{subseteq_antisymmetric}. +\end{proof} + +\begin{lemma}\label{ordinal_elem_connex_step} + Let $\alpha,\gamma$ be ordinals. + Suppose for all sets $\xi,\beta$ such that $\xi\in\alpha$ and $\beta$ is an ordinal + we have $\xi\in\beta\lor \beta\in\xi \lor \xi = \beta$. + Then $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $\gamma$] + Follows by \cref{ordinal_elem_connex_from_elements,elem_of_ordinal_is_ordinal}. +\end{proof} + \begin{proposition}\label{ordinal_elem_connex} - For all ordinals $\alpha,\beta$ + Let $\alpha$ be an ordinal. + Then for every ordinal $\beta$ we have $\alpha\in\beta\lor \beta\in\alpha \lor \alpha = \beta$. \end{proposition} \begin{proof}[Proof by \in-induction on $\alpha$] - % Ind hypothesis: - % ![Xi,Xbeta]:(elem(Xi,falpha)=>((ordinal(Xi)&ordinal(Xbeta))=>(elem(Xi,Xbeta)|elem(Xbeta,Xi)|Xi=Xbeta)))) - % Goal: - % ordinal(falpha)&ordinal(fbeta))=>(elem(falpha,fbeta)|elem(fbeta,falpha)|falpha=fbeta) - % - Assume $\alpha$ is an ordinal. - Show for all ordinals $\gamma$ we have $\alpha\in\gamma\lor \gamma\in\alpha \lor \alpha = \gamma$. - \begin{subproof}[Proof by \in-induction on $\gamma$] - % Now we have: - % ![Xi]:(elem(Xi,fgamma)=>(ordinal(Xi)=>(elem(falpha,Xi)|elem(Xi,falpha)|falpha=Xi)))). - % Goal: ordinal(fgamma)=>(elem(falpha,fgamma)|elem(fgamma,falpha)|falpha=fgamma)) - % - Assume $\gamma$ is an ordinal. - Follows by \cref{setext,transitiveset,ordinal}. - \end{subproof} + Follows by \cref{ordinal_elem_connex_step,elem_of_ordinal_is_ordinal}. \end{proof} \begin{proposition}\label{ordinal_proper_subset_implies_elem} @@ -245,20 +311,24 @@ To show that \in\ is a strict total order it only remains to show that \in\ is c Then $\alpha\in\beta$. \end{proposition} \begin{proof} - $\beta\setminus\alpha$ is inhabited. - Take $\gamma$ such that $\gamma$ is an \in-minimal element of $\beta\setminus\alpha$. + $\beta\setminus\alpha$ is inhabited + by \cref{difference_with_proper_subset_is_inhabited}. + Take $\gamma$ such that $\gamma$ is an \in-minimal element of $\beta\setminus\alpha$ + by \cref{regularity}. Now $\gamma\in\beta$ by \cref{setminus_elim_left}. - Hence $\gamma\subseteq\beta$ - by \cref{ordinal,transitiveset_iff_subseteq}. - For all $\delta\in\beta\setminus\alpha$ we have $\delta\notin\gamma$. - Thus $\gamma\setminus\alpha = \emptyset$. - Hence $\gamma\subseteq\alpha$. - It suffices to show that for all $\delta\in\alpha$ we have $\delta\in\gamma$. - Suppose not. - Take $\delta\in\alpha$ such that $\delta\notin\gamma$. - Now if $\delta = \gamma$ or $\gamma\in\delta$, then $\gamma\in\alpha$ - % Original Vampire proof: by \cref{ordinal,elem_subseteq,elem_of_ordinal_is_ordinal,setminus_elim_left,ordinal_elem_connex,inter_eq_left_implies_subseteq,inter_absorb_supseteq_left,transitiveset_iff_subseteq}. - by \cref{ordinal,elem_subseteq,elem_of_ordinal_is_ordinal,ordinal_elem_connex,transitiveset_iff_subseteq}. + Thus $\gamma$ is an ordinal by \cref{elem_of_ordinal_is_ordinal}. + Hence $\gamma\subseteq\beta$ by \cref{ordinal_elem_implies_subseteq}. + For all $\delta\in\beta\setminus\alpha$ we have $\delta\notin\gamma$ + by \cref{disjoint}. + Thus $\gamma\setminus\alpha = \emptyset$ + by \cref{setext,setminus_intro,setminus_elim_left,setminus_elim_right,elem_subseteq}. + Hence $\gamma\subseteq\alpha$ + by \cref{setminus_eq_emptyset_iff_subseteq}. + For all $\delta\in\alpha$ we have $\delta\in\gamma$ + by \cref{ordinal_elem_connex,ordinal_is_transitiveset,elem_of_ordinal_is_ordinal,transitiveset_iff_subseteq,elem_subseteq,setminus_elim_right}. + Thus $\alpha\subseteq\gamma$ by \cref{subseteq}. + Thus $\alpha = \gamma$ by \cref{subseteq_antisymmetric}. + Follows by assumption. \end{proof} \begin{proposition}\label{ordinal_elem_implies_proper_subset} @@ -267,7 +337,7 @@ To show that \in\ is a strict total order it only remains to show that \in\ is c Then $\alpha\subset\beta$. \end{proposition} \begin{proof} - $\alpha\subseteq\beta$. + Follows by \cref{subset,ordinal_elem_implies_subseteq,in_irrefl}. \end{proof} \begin{proposition}\label{ordinal_preceq_implies_subseteq} @@ -276,12 +346,7 @@ Suppose $\alpha\precedeseq\beta$. Then $\alpha\subseteq\beta$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$\alpha = \beta$.} - Trivial. - \caseOf{$\alpha\precedes\beta$.} - $\alpha\subset\beta$. - \end{byCase} + Follows by assumption. \end{proof} %\begin{proposition}% @@ -304,12 +369,18 @@ Then $\alpha\subseteq\beta$. Let $\alpha,\beta$ be ordinals. Then $\alpha\in\beta$ or $\beta\subseteq\alpha$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal_elem_connex,ordinal_elem_implies_subseteq,subseteq}. +\end{proof} \begin{proposition}\label{ordinal_subseteq_or_subseteq} Let $\alpha,\beta$ be ordinals. Then $\alpha\subseteq\beta$ or $\beta\subseteq\alpha$. \end{proposition} +\begin{proof} + Follows by \cref{ordinal_elem_connex,ordinal_elem_implies_subseteq,subseteq}. +\end{proof} \begin{proposition}\label{ordinal_subseteq_implies_elem_or_eq} @@ -317,12 +388,18 @@ Then $\alpha\subseteq\beta$. Suppose $\alpha\subseteq\beta$. Then $\alpha\in\beta$ or $\alpha = \beta$. \end{proposition} +\begin{proof} + Follows by \cref{subset,ordinal_proper_subset_implies_elem}. +\end{proof} \begin{corollary}\label{ordinal_subset_trichotomy} Let $\alpha,\beta$ be ordinals. Then $(\alpha\subset\beta \lor \beta\subset\alpha) \lor \alpha = \beta$. \end{corollary} +\begin{proof} + Follows by \cref{subset,ordinal_elem_connex,ordinal_elem_implies_proper_subset}. +\end{proof} \begin{proposition}\label{ordinal_nor_elem_implies_eq} Let $\alpha,\beta$ be ordinals. @@ -330,16 +407,14 @@ Then $\alpha\subseteq\beta$. Then $\alpha = \beta$. \end{proposition} \begin{proof} - Neither $\alpha\subset\beta$ nor $\beta\subset\alpha$. + Follows by \cref{ordinal_elem_connex}. \end{proof} \begin{proposition}\label{ordinal_in_trichotomy} Let $\alpha,\beta$ be ordinals. Then $(\alpha\in\beta \lor \beta\in\alpha) \lor \alpha = \beta$. \end{proposition} \begin{proof} - Suppose not. - Then neither $\alpha\in\beta$ nor $\beta\in\alpha$. - Thus $\alpha = \beta$ by \cref{ordinal_nor_elem_implies_eq}. Contradiction. + Follows by \cref{ordinal_elem_connex}. \end{proof} \begin{corollary}\label{ordinal_prec_trichotomy} @@ -354,6 +429,9 @@ Then $\alpha\subseteq\beta$. \begin{corollary}\label{ordinal_elem_or_superset} Let $\alpha,\beta$ be ordinals. Then $\alpha\in \beta$ or $\beta\subseteq \alpha$. \end{corollary} +\begin{proof} + Follows by \cref{ordinal_elem_or_subseteq}. +\end{proof} @@ -362,6 +440,9 @@ Then $\alpha\subseteq\beta$. \begin{proposition}\label{emptyset_is_ordinal} $\emptyset$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal,transitiveset,emptyset}. +\end{proof} % The proof of this theorem benefits from the alternate definition of % transitivity in terms of $\subseteq$. @@ -371,22 +452,33 @@ Then $\alpha\subseteq\beta$. \end{proposition} \begin{proof} $\suc{\alpha}$ is \in-transitive by \cref{ordinal,suc_of_transitiveset_is_transitiveset}. - For every $\beta\in\alpha$ we have that $\beta$ is \in-transitive. + For every $\beta\in\alpha$ we have that $\beta$ is \in-transitive + by \cref{ordinal,transitiveset}. + Follows by \cref{ordinal,suc_iff}. \end{proof} \begin{proposition}\label{ordinal_iff_suc_ordinal} $\alpha$ is an ordinal iff $\suc{\alpha}$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{suc_ordinal,suc_intro_self,elem_of_ordinal_is_ordinal}. +\end{proof} \begin{proposition}\label{ordinal_in_suc} Let $\alpha$ be an ordinal. Then $\alpha\in\suc{\alpha}$. \end{proposition} +\begin{proof} + Follows by \cref{suc_intro_self}. +\end{proof} \begin{corollary}\label{ordinal_precedes_suc} Let $\alpha$ be an ordinal. Then $\alpha\precedes \suc{\alpha}$. \end{corollary} +\begin{proof} + Follows by \cref{suc_ordinal,ordinal_in_suc}. +\end{proof} \begin{proposition}\label{ordinal_elem_implies_subset_of_suc} Let $\alpha,\beta$ be ordinals. @@ -394,9 +486,7 @@ Then $\alpha\subseteq\beta$. Then $\alpha\subseteq\suc{\beta}$. \end{proposition} \begin{proof} - $\alpha\subset \beta$. - In particular, $\alpha\subseteq \beta$. - Hence $\alpha\subseteq \cons{\beta}{\beta}$. + Follows by \cref{ordinal_elem_implies_subseteq,subseteq_self_suc_intro,subseteq_transitive}. \end{proof} \begin{proposition}\label{unions_of_ordinal_is_ordinal} @@ -406,8 +496,10 @@ Then $\alpha\subseteq\beta$. \begin{proof} For all $x, y$ such that $x\in y\in \unions{\alpha}$ we have $x\in \unions{\alpha}$ by \cref{unions_intro,unions_iff,transitiveset,ordinal}. - Thus $\unions{\alpha}$ is \in-transitive. - Every element of $\unions{\alpha}$ is \in-transitive. + Thus $\unions{\alpha}$ is \in-transitive by \cref{transitiveset}. + Every element of $\unions{\alpha}$ is \in-transitive + by \cref{unions_iff,ordinal,transitiveset}. + Follows by \cref{ordinal}. \end{proof} \begin{lemma}\label{ordinal_subseteq_unions} @@ -430,11 +522,11 @@ Then $\alpha\subseteq\beta$. \end{proof} \begin{proposition}\label{ordinal_empty_or_emptyset_elem} - For all ordinals $\alpha$ - we have $\alpha=\emptyset$ or $\emptyset\in\alpha$. + Let $\alpha$ be an ordinal. + Then $\alpha=\emptyset$ or $\emptyset\in\alpha$. \end{proposition} -\begin{proof}[Proof by \in-induction] - Straightforward. +\begin{proof}[Proof by \in-induction on $\alpha$] + Follows by \cref{setext,emptyset,elem_of_ordinal_is_ordinal,ordinal_transitivity}. \end{proof} \begin{proposition}\label{transitive_set_of_ordinals_is_ordinal} @@ -443,6 +535,9 @@ Then $\alpha\subseteq\beta$. Suppose that $A$ is \in-transitive. Then $A$ is an ordinal. \end{proposition} +\begin{proof} + Follows by \cref{ordinal}. +\end{proof} % Apparently Russel first noticed this antimony while reading a paper by Burali-Forti. % Typographic NB: Cesare Burali-Forti is a single person, therefore only a single hyphen! @@ -451,13 +546,17 @@ Then $\alpha\subseteq\beta$. for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. \end{theorem} \begin{proof} - Suppose not. - Take $\Omega$ such that for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. - For all $x, y$ such that $x\in y\in \Omega$ we have $x\in \Omega$. - Thus $\Omega$ is \in-transitive. - Thus $\Omega$ is an ordinal. - Therefore $\Omega\in\Omega$. - Contradiction. + Assume there exists a set $\Omega$ such that + for all $\alpha$ we have $\alpha\in \Omega$ iff $\alpha$ is an ordinal. + Take $\Omega$ such that for all $\alpha$ we have + $\alpha\in \Omega$ iff $\alpha$ is an ordinal by assumption. + For all $x, y$ such that $x\in y\in \Omega$ we have $x\in \Omega$ + by \cref{elem_of_ordinal_is_ordinal}. + Thus $\Omega$ is \in-transitive by \cref{transitiveset}. + For every $\alpha\in\Omega$ we have $\alpha$ is an ordinal by assumption. + Thus $\Omega$ is an ordinal by \cref{ordinal}. + Therefore $\Omega\in\Omega$ by assumption. + Contradiction by \cref{in_irrefl}. \end{proof} \begin{proposition}\label{inters_of_ordinals_is_ordinal} @@ -466,7 +565,13 @@ Then $\alpha\subseteq\beta$. Then $\inters{A}$ is an ordinal. \end{proposition} \begin{proof} - It suffices to show that $\inters{A}$ is \in-transitive. + For all $x,y$ such that $x\in y\in\inters{A}$ we have $x\in\inters{A}$ + by \cref{inters_iff_forall,ordinal_transitivity}. + Thus $\inters{A}$ is \in-transitive by \cref{transitiveset}. + Take $\alpha$ such that $\alpha\in A$ by assumption. + For every $y\in\inters{A}$ we have $y$ is an ordinal + by \cref{inters_iff_forall,elem_of_ordinal_is_ordinal}. + Follows by \cref{ordinal}. \end{proof} \begin{proposition}\label{inters_of_ordinals_subseteq} @@ -474,6 +579,9 @@ Then $\alpha\subseteq\beta$. Suppose for every $\alpha\in A$ we have $\alpha$ is an ordinal. Then for all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. \end{proposition} +\begin{proof} + Follows by \cref{inters_subseteq_elem}. +\end{proof} \begin{proposition}\label{inters_of_ordinals_elem} Let $A$ be an inhabited set. @@ -491,7 +599,12 @@ Then $\alpha\subseteq\beta$. Then $\inters{A}$ is an \in-minimal element of $A$. \end{proposition} \begin{proof} - For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. + $\inters{A}\in A$ by \cref{inters_of_ordinals_elem}. + For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$ + by \cref{inters_of_ordinals_subseteq}. + For all $\delta\in\inters{A}$ we have $\delta\notin A$ + by \cref{elem_of_ordinal_is_ordinal,ordinal_elem_implies_proper_subset,subset,subseteq_antisymmetric}. + Follows by \cref{disjoint}. \end{proof} \begin{proposition}\label{inters_of_ordinals_is_minimal_alternate} @@ -500,7 +613,7 @@ Then $\alpha\subseteq\beta$. Then for all $\alpha\in A$ we have $\inters{A} = \alpha$ or $\inters{A}\in\alpha$. \end{proposition} \begin{proof} - For all $\alpha\in A$ we have $\inters{A}\subseteq \alpha$. + Follows by \cref{inters_of_ordinals_is_ordinal,inters_of_ordinals_subseteq,ordinal_subseteq_implies_elem_or_eq}. \end{proof} \begin{proposition}\label{inter_of_two_ordinals_is_ordinal} @@ -534,27 +647,28 @@ Then $\alpha\subseteq\beta$. Then $\alpha$ is a limit ordinal or $\alpha$ is a successor ordinal. \end{lemma} \begin{proof} - \begin{byCase} - \caseOf{$\alpha$ is a limit ordinal.} - Trivial. - \caseOf{$\alpha$ is not a limit ordinal.} - Take $\beta$ such that $\beta\in\alpha$ and $\suc{\beta}\notin\alpha$ - by \cref{limit_ordinal}. - \end{byCase} + Assume $\alpha$ is not a limit ordinal. + Take $\beta$ such that $\beta\in\alpha$ and $\suc{\beta}\notin\alpha$ + by \cref{limit_ordinal}. + Thus $\beta$ is an ordinal by \cref{elem_of_ordinal_is_ordinal}. + Thus $\suc{\beta}$ is an ordinal by \cref{suc_ordinal}. + We have $\alpha=\suc{\beta}$ + by \cref{ordinal_elem_connex,suc_elim,in_asymmetric,in_irrefl}. + Follows by \cref{successor_ordinal}. \end{proof} \begin{lemma}\label{zero_not_successorordinal} $\emptyset$ is not a successor ordinal. \end{lemma} +\begin{proof} + Follows by \cref{successor_ordinal,suc_neq_emptyset}. +\end{proof} \begin{lemma}\label{zero_not_limitordinal} $\emptyset$ is not a limit ordinal. \end{lemma} \begin{proof} - Suppose not. - Then $\emptyset\precedes \emptyset$ by \cref{emptyset,limit_ordinal}. - Thus $\emptyset\in \emptyset$. - Contradiction. + Follows by \cref{limit_ordinal,emptyset,in_irrefl}. \end{proof} \begin{lemma}\label{suc_elem_limitordinal} |