working commit

1 files changed, 65 insertions, 7 deletions

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 83e3aa4..9990199 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -94,6 +94,9 @@
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{nat_is_transitiveset}.
+\end{proof}
 
 \begin{proposition}\label{naturals_elem_in_transitive}
     If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
@@ -119,6 +122,9 @@
 \begin{proposition}\label{zero_is_empty}
     There exists no $x$ such that $x \in \zero$.
 \end{proposition}
+\begin{proof}
+    Follows by \cref{notin_emptyset}.
+\end{proof}
 
 \begin{proposition}\label{one_is_positiv}
     $1$ is positiv.
@@ -163,6 +169,13 @@
     Omitted.
 \end{proof}
 
+\begin{proposition}\label{naturals_one_zero_or_greater}
+    For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}.
+\end{proof}
+
 \begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
     For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
 \end{proposition}
@@ -184,7 +197,7 @@
             \end{subproof}
         \caseOf{$n = 1$.}
             Fix $m$.
-            For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$.
+            For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
             Then $\zero + 1 = 1$.
         \caseOf{$n > 1$.} 
             Take $l \in \naturals$ such that $\suc{l} = n$.
@@ -350,7 +363,7 @@
     Suppose $U$ is a urysohnchain of $X$.
     Suppose $\dom{U}$ is finite.
     Suppose $U$ is inhabited.
-    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $U$ to $V$ and $V$ is normal ordered.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered.
 \end{proposition}
 \begin{proof}
     Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
@@ -360,11 +373,36 @@
         \caseOf{$n \neq \zero$.}
             Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. 
             We have $\dom{U} \subseteq \naturals$.
-            $\dom{U}$ is inhabited.
+            $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}.
+            $\dom{U}$ has cardinality $\suc{k}$.
             We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             \begin{subproof}
-                Omitted.
+                For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+                We have $\dom{U} \subseteq \naturals$.
+                $\dom{U}$ is inhabited.
+                Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
+                We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                \begin{subproof}
+                    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                    \begin{subproof}
+                        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                        Fix $y \in \seq{\emptyset}{k'}$.
+                        Then $y \leq k'$.
+                        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                        %Then $\seq{\emptyset}{k'} \in \suc{k}$.
+                        Therefore $y \in \suc{k}$.
+                        Therefore $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                    \begin{subproof}
+                        Fix $y \in \seq{\emptyset}{k}$.
+                    \end{subproof}
+                \end{subproof}
             \end{subproof}
+            Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
             Let $N = \seq{\zero}{k}$.
             Let $M = \pow{X}$.
             Define $V : N \to M$ such that $V(n)=
@@ -374,11 +412,31 @@
             $\dom{V} = \seq{\zero}{k}$.
             We show that $V$ is a urysohnchain of $X$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                We show that $V$ is a chain of subsets in $X$.
+                \begin{subproof}
+                    It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}.
+                    It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $n \in \dom{V}$.
+                    Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                    It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                    Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                \end{subproof}
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V} \land n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
-            We show that $F$ is consistent on $U$ to $V$.
+            We show that $F$ is consistent on $V$ to $U$.
             \begin{subproof}
-                Trivial.
+                It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}.
+                $F$ is a bijection from $\dom{V}$ to $\dom{U}$.
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
             \end{subproof}
             $V$ is normal ordered.
     \end{byCase}