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 ) ) |