How to write down this simple proof? (in natural numbers, if for every number there is a smaller number then 1 is in the set) This seems undeniably true to me, but I don't know how to write it down.
Given the non-empty set $S$ containing only natural numbers (starting at 1, not 0). If for every number $x$ greater than 1 there is a number $y$ such that $y<x$, then 1 must be in the set $S$.
I think this must be true, because you can start at any natural number, and take a smaller number, and a smaller number than that, smaller than that and so forth, until you arrive at 1. But how do you actually write this proof down?
 A: Using the well ordering principle of $\mathbb N$, as $S$ is nonempty, there is $y\in S$ so that 
$$y\le x\ \ \ \ \ \forall x\in S.$$
If $y\neq 1$, then by the definition of $S$, there is $y_0\in S$ so that $y_0 <y$. But that is impossible by the choice of $y$. Thus $y=1$ and so $1\in S$. 
A: I prefer John Ma’s argument, but if you’re more familiar with the induction axiom than with the well-ordering principle, you may prefer this one:
Suppose that $1\notin S$, and let $A=\big\{n\in\Bbb Z^+:S\cap\{1,\ldots,n\}=\varnothing\big\}$; clearly $1\in A$. Suppose that $n\in A$; then $\{1,\ldots,n\}\cap S=\varnothing$, so $n+1\notin S$. But then $\{1,\ldots,n+1\}\cap S=\varnothing$, so $n+1\in A$. Thus, $1\in A$, and for every $n\in\Bbb Z^+$ we have $n\in A\implies n+1\in A$, so by the induction axiom $A=\Bbb Z^+$. But then $S=\Bbb Z^+\cap S=\varnothing$, contradicting the hypothesis that $S$ is non-empty.
A: $$\begin{align}\text{Let }\mathbb{N}&=\{x\geq1\mid x\in\mathbb{Z}\},\tag{1}\label{defN}\\S&\neq\emptyset\tag{2}\label{defS}\end{align}$$
then we are asked to show that
$$\forall_S:\;(S\subseteq\mathbb{N})\land\forall_{x\in{S}}((x>1)\implies\exists_{y\in{S}}:y<x)\implies1\in{S},$$
which is equivalent to
$$\forall_S:\;1\notin{S}\implies\lnot\Big((S\subseteq\mathbb{N})\land\forall_{x\in{S}}((x>1)\implies\exists_{y\in{S}}:y<x)\Big)$$
by contraposition and hence to
$$\forall_S:\;1\notin{S}\implies(S\not\subseteq\mathbb{N})\lor\lnot\forall_{x\in{S}}((x>1)\implies\exists_{y\in{S}}:y<x).$$
The case of $S\not\subseteq\mathbb{N}$ is uninteresting, so setting $S\subseteq\mathbb{N}$, and by negation of universal quantification we have:
$$\forall_{S\subseteq\mathbb{N}}:\;1\notin{S}\implies\exists_{x\in{S}}\,\lnot((x>1)\implies\exists_{y\in{S}}:y<x),$$
which, negating the material implication, yields:
$$\forall_{S\subseteq\mathbb{N}}:\;1\notin{S}\implies\exists_{x\in{S}}\,((x>1)\land\lnot\exists_{y\in{S}}:y<x),$$
and by negation of existential quantification we have:
$$\forall_{S\subseteq\mathbb{N}}:\;1\notin{S}\implies\exists_{x\in{S}}\,((x>1)\land\forall_{y\in{S}}:y\geq{x}).$$
Indeed, since $1\notin{S}$, we have $x>1$ by the definition of $\mathbb{N}$ in $\eqref{defN}$, so we have:
$$\forall_{S\subseteq\mathbb{N}}:\;1\notin{S}\implies\exists_{x\in{S}}\,\forall_{y\in{S}}:y\geq{x},$$
and, as the consequent $\exists_{x\in{S}}\,\forall_{y\in{S}}:y\geq{x}$ (no matter if $1\in{S}$ or $1\notin{S}$) is precisely what is claimed by the well-ordering principle linked by @John, we conclude the implication is true for all subsets $S$ of the set of natural numbers $\mathbb{N}$.
