Theorem unben

Description: An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005) (Revised by Mario Carneiro, 15-Sep-2013)

	Ref	Expression
Assertion	unben	⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → 𝐴 ≈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
2	1	unbenlem	⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → 𝐴 ≈ ω )
3		nnenom	⊢ ℕ ≈ ω
4	3	ensymi	⊢ ω ≈ ℕ
5		entr	⊢ ( ( 𝐴 ≈ ω ∧ ω ≈ ℕ ) → 𝐴 ≈ ℕ )
6	2 4 5	sylancl	⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → 𝐴 ≈ ℕ )