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 e. _V
Assertion infcntss
|- ( _om ~<_ A -> E. x ( x C_ A /\ x ~~ _om ) )

Proof

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