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 e. dom card /\ -. S e. Fin ) -> _om ~<_ S )

Proof

Step	Hyp	Ref	Expression
1		omelon	|- _om e. On
2		onenon	|- ( _om e. On -> _om e. dom card )
3	1 2	ax-mp	|- _om e. dom card
4		domtri2	|- ( ( _om e. dom card /\ S e. dom card ) -> ( _om ~<_ S <-> -. S ~< _om ) )
5	3 4	mpan	|- ( S e. dom card -> ( _om ~<_ S <-> -. S ~< _om ) )
6		isfinite	|- ( S e. Fin <-> S ~< _om )
7	6	notbii	|- ( -. S e. Fin <-> -. S ~< _om )
8	5 7	bitr4di	|- ( S e. dom card -> ( _om ~<_ S <-> -. S e. Fin ) )
9	8	biimpar	|- ( ( S e. dom card /\ -. S e. Fin ) -> _om ~<_ S )