最小元の存在

名前はもっといいのがあるかも

$ \forall A\in 2^\N\setminus\{\varnothing\}\exist m\in A\forall n\in A:m\le n

証明

$ \lnot\forall A\in2^\N:(1\in A\land\forall n\in A:\operatorname{succ}(n)\in A\implies A=\N)

$ \iff\exist A\in 2^\N:(1\in A\land\forall n\in A:\operatorname{succ}(n)\in A\land\exist n\in\N:n\notin A)

$ \implies\exist A\in 2^\N\begin{dcases}1\in A\land\forall n\in A:\operatorname{succ}(n)\in A\\\exist m\in\N\setminus A\forall n\in\N\setminus A:m\le n\end{dcases}

$ \iff\exist A\in 2^\N\begin{dcases}1\in A\land\forall n\in A:\operatorname{succ}(n)\in A\\\exist m\in\N:m\notin A\land\forall n\in\N:(n\notin A\implies m\le n)\end{dcases}

$ \iff\exist A\in 2^\N\begin{dcases}1\in A\land\forall n\in A:\operatorname{succ}(n)\in A\\\exist m\in\N:m\notin A\land\forall n\in\N_{<m}:n\in A\end{dcases}

$ \implies\exist A\in 2^\N\begin{dcases}\forall n\in A:\operatorname{succ}(n)\in A\\\exist m\in\N\setminus\{1\}:m\notin A\land\forall n\in\N_{<m}:n\in A\end{dcases}

$ \implies\exist A\in 2^\N\begin{dcases}\forall n\in A:\operatorname{succ}(n)\in A\\m\notin A\land(m-1)\in A\end{dcases}

$ \implies\exist A\in 2^\N\exist m\in\N\setminus\{1\}\begin{dcases}\operatorname{succ}(m-1)=m\in A\\\exist m\in\N\setminus\{1\}:m\notin A\land(m-1)\in A\end{dcases}

$ \implies\bot

$ \underline{\therefore\forall A\in2^\N:(1\in A\land\forall n\in A:\operatorname{succ}(n)\in A\implies A=\N)\quad}_\blacksquare

$ \lnot\forall A\in 2^\N\setminus\{\varnothing\}\exist m\in A\forall n\in A:m\le n

$ \iff\exist A\in2^N\setminus\{\varnothing\}\forall m\in A\exist n\in A:m>n

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\1\in \{n\in\N\mid\N_{<n}\cap A=\varnothing\}\land(\forall n\in \{n\in\N\mid\N_{<n}\cap A=\varnothing\}:\operatorname{succ}(n)\in \{n\in\N\mid\N_{<n}\cap A=\varnothing\})\implies \{n\in\N\mid\N_{<n}\cap A=\varnothing\}=\N\end{dcases}

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\\N_{<1}\cap A=\varnothing\land\forall n\in\N:(\N_{<n}\cap A=\varnothing\implies\N_{<\operatorname{succ}(n)}\cap A=\varnothing)\implies \{n\in\N\mid\N_{<n}\cap A=\varnothing\}=\N\end{dcases}

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\\forall n\in\N:(\N_{<n}\cap A=\varnothing\implies\N_{<\operatorname{succ}(n)}\cap A=\varnothing)\implies \{n\in\N\mid\N_{<n}\cap A=\varnothing\}=\N\end{dcases}

$ \because\N_{<1}=\varnothing

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\\forall n\in\N:(\N_{<n}\cap A=\varnothing\implies\N_{<\operatorname{succ}(n)}\cap A=\varnothing)\implies \{n\in\N\mid\N_{<n}\cap A=\varnothing\}=\N\\\forall n\in\N:\end{dcases}

$ \N_{<n}\cap A=\varnothing

$ \iff\forall a\in A:n\le a

$ \implies\forall a\in A\exist m\in A:n\le a\land m< a

$ \because \forall m\in A\exist n\in A:m>n

$ \implies\forall a\in A\exist m\in A:n\le m< a

$ \iff\forall a\in A\exist m\in A:n+1\le m+1\le a

$ \implies\forall a\in A:n+1

$ \iff\N_{<\operatorname{succ}(n)}\cap A=\varnothing

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\\{n\in\N\mid\N_{<n}\cap A=\varnothing\}=\N\end{dcases}

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\\forall n\in\N:\N_{<n}\cap A=\varnothing\end{dcases}

$ \iff\exist A\in2^N\setminus\{\varnothing\}\begin{dcases}\forall m\in A\exist n\in A:m>n\\\forall n\in\N\forall a\in A:n\le a\end{dcases}

$ \implies\exist A\in2^N\setminus\{\varnothing\}\forall m\in A\exist n\in A:m>n\land m\le n

$ \iff\bot

$ \underline{\therefore\forall A\in 2^\N\setminus\{\varnothing\}\exist m\in A\forall n\in A:m\le n\quad}_\blacksquare

Reference

これよく読んで証明書いてた覚えある