Metamath Proof Explorer

Theorem zct

Description: The set of integer numbers is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion zct 
|- ZZ ~<_ _om

Proof

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