blob: 377604591d120ad9da2caf712aabf1ddce80c8ad (
plain)
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
|
\import{set/cons.tex}
\import{set/regularity.tex}
\subsection{Successor}
\begin{definition}\label{suc}
$\suc{x} = \cons{x}{x}$.
\end{definition}
\begin{proposition}\label{suc_intro_self}
$x\in\suc{x}$.
\end{proposition}
\begin{proposition}\label{suc_intro_in}
Suppose $x\in y$. Then $x\in\suc{y}$.
\end{proposition}
\begin{proposition}\label{suc_elim}
Suppose $x\in\suc{y}$.
Then $x = y$ or $x\in y$.
\end{proposition}
\begin{proposition}\label{suc_iff}
$x\in\suc{y}$ iff $x = y$ or $x\in y$.
\end{proposition}
\begin{proposition}\label{suc_neq_emptyset}
$\suc{x}\neq \emptyset$.
\end{proposition}
\begin{proposition}\label{suc_subseteq_implies_in}
Suppose $\suc{x}\subseteq y$. Then $x\in y$.
\end{proposition}
\begin{proposition}\label{suc_neq_self}
$\suc{x}\neq x$.
\end{proposition}
\begin{proposition}\label{suc_injective}
Suppose $\suc{x} = \suc{y}$. Then $x = y$.
\end{proposition}
\begin{proof}
Suppose not.
$\suc{x}\subseteq \suc{y}$. Hence $x\in\suc{y}$.
Then $x\in y$.
$\suc{y}\subseteq \suc{x}$. Hence $y\in\suc{x}$.
Then $y\in x$.
Contradiction.
\end{proof}
\begin{proposition}\label{subseteq_self_suc_intro}
$x\subseteq\suc{x}$.
\end{proposition}
\begin{proposition}\label{suc_subseteq_intro}
Suppose $x\in y$ and $x\subseteq y$.
Then $\suc{x}\subseteq y$.
\end{proposition}
\begin{proposition}\label{suc_subseteq_elim}
Suppose $\suc{x}\subseteq y$.
Then $x\in y$ and $x\subseteq y$.
\end{proposition}
\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}
|
