公理的集合論における自然数の存在(その 4)

いよいよ、自然数に大小を定義したいのですが、その前に、一つ補題を示します。

補題

任意の自然数 $m,n\in\omega$ について $m\in n\leftrightarrow m\subset n$ *1

(証明)
$P_1(n)\equiv\forall m\in\omega(m\in n\to m\subset n)$
$P_2(n)\equiv\forall m\in\omega(m\subset n\to m\in n)$
とおく。 $m\in\emptyset$ と $m\subset\emptyset$ はともに偽だから、 $P_1(0),P_2(0)$ はともに真。
$P_1(n)\to P_1(n^+)$ を示す。 $m\in n^+=n\cup\{n\}$ ならば $m\in n\vee m=n$ である。 $m\in n$ ならば $P_1(n)$ により $m\subset n$ であるから、 $n\subset n^+$ により、いずれの場合も $m\subset n^+$ が成り立つ。以上で数学的帰納法により $P_1(n)$ は $\forall n\in\omega$ に対して真。
$P_2(n)\to P_2(n^+)$ を示す。 $m\subset n^+$ として $n\in m$ と仮定すると、 $P_1(m)$ により $n\subset m$ であるから $n^+=n\cup\{n\}\subseteq m$ であるが、これは $m\subset n^+$ に矛盾する。よって $n\not\in m$ であるから、 $m\subset n^+=n\cup\{n\}$ と合わせて $m\subseteq n$ を得る。 $m\subset n$ ならば $P_2(n)$ により $m\in n$ となるから $m\in n^+=n\cup\{n\}$ であるし、 $m=n$ ならば明らかに $n\in n^+=n\cup\{n\}$ であるから、合わせて $m\in n^+$ を得る。以上で数学的帰納法により $P_2(n)$ は $\forall n\in\omega$ に対して真。
$\forall n\in\omega(P_1(n)\wedge P_2(n))$ を整理して、補題が示される。

*1:ここで $m\subset n$ は $m\subseteq n$ かつ $m\neq n$ の意味ですので注意。