Permalink
Browse files

setmath: empty vs nonempty

  • Loading branch information...
1 parent aedeca6 commit d96eb8bbfe794907b24eb5182405717d2ffb7ddd @mikeshulman mikeshulman committed Dec 15, 2012
Showing with 4 additions and 3 deletions.
  1. +4 −3 ordcard.tex
View
7 ordcard.tex
@@ -291,7 +291,8 @@ \section{Ordinal numbers}
We prove by induction on $<$ that $f(a)=a$ for all $a:A$.
The inductive hypothesis is that for all $a'<a$, we have $f(a')=a'$.
- Now by extensionality, to conclude $f(a)=a$ it is sufficient to show $\prd{c:A}(c<f(a)) \leftrightarrow (c<a)$.
+ Now since $A$ is extensional, to conclude $f(a)=a$ it is sufficient to show
+ \[\prd{c:A}(c<f(a)) \leftrightarrow (c<a).\]
However, since $f$ is an automorphism, we have $(c<a) \leftrightarrow (f(c)<f(a))$.
But $c<a$ implies $f(c)=c$ by the induction hypothesis, so $(c<a) \to (c<f(a))$.
On the other hand, if $c<f(a)$, then $f^{-1}(c)<a$, and so $c = f(f^{-1}(c)) = f^{-1}(c)$ by the induction hypothesis again; thus $c<a$.
@@ -564,8 +565,8 @@ \section{Classical well-orderings}
since if $B:\ord$ and $(g_\ord(B) \in X)$, then $B = Hx$ for some $x:X'$, hence $B<D$.
Now if
\[\setof{ g_\ord(B) | \rule{0pt}{1em} B:\ord \wedge (g_\ord(B) \in X)}\]
- is nonempty, then $g_\ord(D)$ would lie in $X$ but not in this subset, which would be a contradiction since $D$ is itself a potential value for $B$.
- So this set must be empty, hence $g_\ord'$ is surjective as well as injective.
+ is not all of $X$, then $g_\ord(D)$ would lie in $X$ but not in this subset, which would be a contradiction since $D$ is itself a potential value for $B$.
+ So this set must be all of $X$, and hence $g_\ord'$ is surjective as well as injective.
Thus, we can transport the ordinal structure on $\ord'$ to $X$.
\end{proof}

0 comments on commit d96eb8b

Please sign in to comment.