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 S dom card ¬ S Fin ω S

Proof

Step Hyp Ref Expression
1 omelon ω On
2 onenon ω On ω dom card
3 1 2 ax-mp ω dom card
4 domtri2 ω dom card S dom card ω S ¬ S ω
5 3 4 mpan S dom card ω S ¬ S ω
6 isfinite S Fin S ω
7 6 notbii ¬ S Fin ¬ S ω
8 5 7 bitr4di S dom card ω S ¬ S Fin
9 8 biimpar S dom card ¬ S Fin ω S