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	$$⊢\left(A\subseteq \mathbb{N}\wedge \forall m\in \mathbb{N}\exists n\in Am<n\right)\to A\approx \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),1\right)\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),1\right)\upharpoonright }_{\mathrm{\omega }}$$
2	1	unbenlem	$$⊢\left(A\subseteq \mathbb{N}\wedge \forall m\in \mathbb{N}\exists n\in Am<n\right)\to A\approx \mathrm{\omega }$$
3		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
4	3	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
5		entr	$$⊢\left(A\approx \mathrm{\omega }\wedge \mathrm{\omega }\approx \mathbb{N}\right)\to A\approx \mathbb{N}$$
6	2 4 5	sylancl	$$⊢\left(A\subseteq \mathbb{N}\wedge \forall m\in \mathbb{N}\exists n\in Am<n\right)\to A\approx \mathbb{N}$$