Theorem fzoct

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

	Ref	Expression
Assertion	fzoct	⊢ ( 𝑁 ..^ 𝑀 ) ≼ ω

Proof

Step	Hyp	Ref	Expression
1		fzossz	⊢ ( 𝑁 ..^ 𝑀 ) ⊆ ℤ
2		zct	⊢ ℤ ≼ ω
3		ssct	⊢ ( ( ( 𝑁 ..^ 𝑀 ) ⊆ ℤ ∧ ℤ ≼ ω ) → ( 𝑁 ..^ 𝑀 ) ≼ ω )
4	1 2 3	mp2an	⊢ ( 𝑁 ..^ 𝑀 ) ≼ ω