Metamath Proof Explorer

Theorem fzoct

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

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

Proof

Step Hyp Ref Expression
1 fzossz 
 |-  ( 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