Update iso.tex

Changed \olref[sfr][rel][ord]{prop:extensionality-totalorders} to \olref[sfr][rel][ord]{prop:extensionality-strictlinearorders} based on "total order" definition fixes.

Author: gabelthompson

content/set-theory/ordinals/iso.tex

@@ -53,7 +53,7 @@
 
 Generalising, $(\forall x \in B)(x \lessdot f(a) \liff x \lessdot
 g(a))$. It follows that $f(a) = g(a)$ by
-\olref[sfr][rel][ord]{prop:extensionality-totalorders}. So $(\forall
+\olref[sfr][rel][ord]{prop:extensionality-strictlinearorders}. So $(\forall
 a \in A)f(a) = g(a)$ by \olref[wo]{propwoinduction}.
 \end{proof}\noindent 
 This gives some sense that well-orderings are robust. But to continue
@@ -79,7 +79,7 @@
 $f$ is a bijection and $A_a \subsetneq A$, using \olref[wo]{wo:strictorder} let $b \in A$ be the
 $<$-least !!{element} of $A$ such that $b \neq f(b)$. We'll show that
 $(\forall x \in A)(x<b \liff x < f(b))$, from which it will follow by
-\olref[sfr][rel][ord]{prop:extensionality-totalorders} that $b =
+\olref[sfr][rel][ord]{prop:extensionality-strictlinearorders} that $b =
 f(b)$, completing the reductio.
 
 Suppose $x < b$. So $x = f(x)$, by the choice of $b$. And $f(x) <