This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		nnuz	⊢ ℕ = ( ℤ_≥ ‘ 1 )
2	1	sseq2i	⊢ ( 𝐴 ⊆ ℕ ↔ 𝐴 ⊆ ( ℤ_≥ ‘ 1 ) )
3		uzwo	⊢ ( ( 𝐴 ⊆ ( ℤ_≥ ‘ 1 ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )
4	2 3	sylanb	⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 )