Theorem infcntss

Description: Every infinite set has a denumerable subset. Similar to Exercise 8 of TakeutiZaring p. 91. (However, we need neither AC nor the Axiom of Infinity because of the way we express "infinite" in the antecedent.) (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Hypothesis	infcntss.1	$$⊢A\in \mathrm{V}$$
Assertion	infcntss	$$⊢\mathrm{\omega }\preccurlyeq A\to \exists x\left(x\subseteq A\wedge x\approx \mathrm{\omega }\right)$$

Proof

Step	Hyp	Ref	Expression
1		infcntss.1	$$⊢A\in \mathrm{V}$$
2	1	domen	$$⊢\mathrm{\omega }\preccurlyeq A\leftrightarrow \exists x\left(\mathrm{\omega }\approx x\wedge x\subseteq A\right)$$
3		ensym	$$⊢\mathrm{\omega }\approx x\to x\approx \mathrm{\omega }$$
4	3	anim1ci	$$⊢\left(\mathrm{\omega }\approx x\wedge x\subseteq A\right)\to \left(x\subseteq A\wedge x\approx \mathrm{\omega }\right)$$
5	4	eximi	$$⊢\exists x\left(\mathrm{\omega }\approx x\wedge x\subseteq A\right)\to \exists x\left(x\subseteq A\wedge x\approx \mathrm{\omega }\right)$$
6	2 5	sylbi	$$⊢\mathrm{\omega }\preccurlyeq A\to \exists x\left(x\subseteq A\wedge x\approx \mathrm{\omega }\right)$$