Theorem nnct

Description: NN is countable. (Contributed by Thierry Arnoux, 29-Dec-2016)

	Ref	Expression
Assertion	nnct	|- NN ~<_ _om

Proof

Step	Hyp	Ref	Expression
1		nnenom	|- NN ~~ _om
2		endom	|- ( NN ~~ _om -> NN ~<_ _om )
3	1 2	ax-mp	|- NN ~<_ _om