Metamath Proof Explorer


Theorem numinfctb

Description: A numerable infinite set contains a countable subset.MOVABLE (Contributed by Stefan O'Rear, 9-Jul-2015)

Ref Expression
Assertion numinfctb Sdomcard¬SFinωS

Proof

Step Hyp Ref Expression
1 omelon ωOn
2 onenon ωOnωdomcard
3 1 2 ax-mp ωdomcard
4 domtri2 ωdomcardSdomcardωS¬Sω
5 3 4 mpan SdomcardωS¬Sω
6 isfinite SFinSω
7 6 notbii ¬SFin¬Sω
8 5 7 bitr4di SdomcardωS¬SFin
9 8 biimpar Sdomcard¬SFinωS