Theorem nnwo

Description: Well-ordering principle: any nonempty set of positive integers has a least element. Theorem I.37 (well-ordering principle) of Apostol p. 34. (Contributed by NM, 17-Aug-2001)

	Ref	Expression
Assertion	nnwo	$$⊢\left(A\subseteq \mathbb{N}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\le y$$

Proof

Step	Hyp	Ref	Expression
1		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
2	1	sseq2i	$$⊢A\subseteq \mathbb{N}\leftrightarrow A\subseteq {\mathbb{Z}}_{\ge 1}$$
3		uzwo	$$⊢\left(A\subseteq {\mathbb{Z}}_{\ge 1}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\le y$$
4	2 3	sylanb	$$⊢\left(A\subseteq \mathbb{N}\wedge A\ne \varnothing \right)\to \exists x\in A\forall y\in Ax\le y$$