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 e. _V |
|
Assertion | infcntss | |- ( _om ~<_ A -> E. x ( x C_ A /\ x ~~ _om ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infcntss.1 | |- A e. _V |
|
2 | 1 | domen | |- ( _om ~<_ A <-> E. x ( _om ~~ x /\ x C_ A ) ) |
3 | ensym | |- ( _om ~~ x -> x ~~ _om ) |
|
4 | 3 | anim1ci | |- ( ( _om ~~ x /\ x C_ A ) -> ( x C_ A /\ x ~~ _om ) ) |
5 | 4 | eximi | |- ( E. x ( _om ~~ x /\ x C_ A ) -> E. x ( x C_ A /\ x ~~ _om ) ) |
6 | 2 5 | sylbi | |- ( _om ~<_ A -> E. x ( x C_ A /\ x ~~ _om ) ) |