blob: 440467de92872a9306fa65a0107f0721a38c9c17 (
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
|
\import{set.tex}
\section{Regularity}
\begin{abbreviation}\label{elemminimal}
$a$ is an \in-minimal element of $A$ iff
$a\in A$ and $a\notmeets A$.
\end{abbreviation}
% We need to first state regularity in this slightly weirder form,
% so that we can do \in-induction.
\begin{lemma}\label{regularity_aux}
Suppose $a\in A$.
Then there exists $b\in A$ such that
$b\notmeets A$.
\end{lemma}
\begin{proof}[Proof by \in-induction on $a$]
Follows by \cref{disjoint}.
\end{proof}
\begin{proposition}[Regularity]%
\label{regularity}
Let $A$ be an inhabited set.
Then there exists a \in-minimal element of $A$.
\end{proposition}
\begin{proof}
Follows by \cref{regularity_aux}.
\end{proof}
% Isabelle/ZF-style foundation for case analysis
\begin{theorem}[Foundation]\label{foundation}
Let $A$ be a set.
Then $A = \emptyset$ or there exists $a\in A$
such that for all $x\in a$ we have $x\notin A$.
\end{theorem}
\begin{proof}
Follows by \cref{nonempty_inhabited,regularity,disjoint}.
\end{proof}.
\begin{proposition}\label{in_irrefl}
For all sets $A$ we have $A\not\in A$.
\end{proposition}
\begin{proof}
Follows by \cref{foundation,upair_iff}.
\end{proof}
\begin{proposition}\label{in_asymmetric}
For all sets $a, b$ such that $a\in b$ we have $b\notin a$.
\end{proposition}
\begin{proof}
Follows by \cref{foundation,upair_iff}.
\end{proof}
|
