Metamath Proof Explorer


Theorem zct

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

Ref Expression
Assertion zct ⊢ ℤ ≼ ω

Proof

Step Hyp Ref Expression
1 zenom ⊢ ℤ ≈ ω
2 endom ⊢ ℤ ≈ ω → ℤ ≼ ω
3 1 2 ax-mp ⊢ ℤ ≼ ω