1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
\import{set/cons.tex}
\import{set/regularity.tex}
\subsection{Ordinal successor}
\begin{definition}\label{suc}
$\suc{x} = \unions{\upair{\upair{x}{x}}{x}}$.
\end{definition}
\begin{proposition}\label{suc_intro_self}
$x\in\suc{x}$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff}.
\end{proof}
\begin{proposition}\label{suc_intro_in}
Suppose $x\in y$. Then $x\in\suc{y}$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff}.
\end{proof}
\begin{proposition}\label{suc_elim}
Suppose $x\in\suc{y}$.
Then $x = y$ or $x\in y$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff}.
\end{proof}
\begin{proposition}\label{suc_iff}
$x\in\suc{y}$ iff $x = y$ or $x\in y$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff}.
\end{proof}
\begin{proposition}\label{suc_neq_emptyset}
$\suc{x}\neq \emptyset$.
\end{proposition}
\begin{proof}
Follows by \cref{suc_intro_self}.
\end{proof}
\begin{proposition}\label{suc_subseteq_implies_in}
Suppose $\suc{x}\subseteq y$. Then $x\in y$.
\end{proposition}
\begin{proof}
Follows by \cref{subseteq,suc_intro_self}.
\end{proof}
\begin{proposition}\label{suc_neq_self}
$\suc{x}\neq x$.
\end{proposition}
\begin{proof}
Follows by \cref{suc_intro_self,in_irrefl}.
\end{proof}
\begin{proposition}\label{suc_injective}
Suppose $\suc{x} = \suc{y}$. Then $x = y$.
\end{proposition}
\begin{proof}
Follows by \cref{suc_intro_self,suc_elim,in_asymmetric}.
\end{proof}
\begin{proposition}\label{subseteq_self_suc_intro}
$x\subseteq\suc{x}$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff,subseteq}.
\end{proof}
\begin{proposition}\label{suc_subseteq_intro}
Suppose $x\in y$ and $x\subseteq y$.
Then $\suc{x}\subseteq y$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff,subseteq}.
\end{proof}
\begin{proposition}\label{suc_subseteq_elim}
Suppose $\suc{x}\subseteq y$.
Then $x\in y$ and $x\subseteq y$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,cons_iff,subseteq}.
\end{proof}
\begin{proposition}\label{suc_next_subset}
There exists no $z$ such that $x\subset z\subset \suc{x}$.
\end{proposition}
\begin{proof}
Follows by \cref{suc,subset,subseteq,subset_witness,suc_elim}.
\end{proof}
|
