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 | ||
Assertion | infcntss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infcntss.1 | ||
2 | 1 | domen | |
3 | ensym | ||
4 | 3 | anim1ci | |
5 | 4 | eximi | |
6 | 2 5 | sylbi |