Metamath Proof Explorer

Theorem fzct

Description: A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion fzct 
|- ( N ... M ) ~<_ _om

Proof

Step Hyp Ref Expression
1 fzssz 
 |-  ( N ... M ) C_ ZZ
2 zct 
 |-  ZZ ~<_ _om
3 ssct 
 |-  ( ( ( N ... M ) C_ ZZ /\ ZZ ~<_ _om ) -> ( N ... M ) ~<_ _om )
4 1 2 3 mp2an 
 |-  ( N ... M ) ~<_ _om