Metamath Proof Explorer


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 V
Assertion infcntss ω A x x A x ω

Proof

Step Hyp Ref Expression
1 infcntss.1 A V
2 1 domen ω A x ω x x A
3 ensym ω x x ω
4 3 anim1ci ω x x A x A x ω
5 4 eximi x ω x x A x x A x ω
6 2 5 sylbi ω A x x A x ω