Theorem fz1nnct

Description: NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020)

	Ref	Expression
Assertion	fz1nnct	$$⊢\left(A=\mathbb{N}\vee A=\left(1..^M\right)\right)\to A\preccurlyeq \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		nnct	$$⊢\mathbb{N}\preccurlyeq \mathrm{\omega }$$
2		breq1	$$⊢A=\mathbb{N}\to \left(A\preccurlyeq \mathrm{\omega }\leftrightarrow \mathbb{N}\preccurlyeq \mathrm{\omega }\right)$$
3	1 2	mpbiri	$$⊢A=\mathbb{N}\to A\preccurlyeq \mathrm{\omega }$$
4		fzofi	$$⊢\left(1..^M\right)\in \mathrm{Fin}$$
5		fict	$$⊢\left(1..^M\right)\in \mathrm{Fin}\to \left(1..^M\right)\preccurlyeq \mathrm{\omega }$$
6	4 5	ax-mp	$$⊢\left(1..^M\right)\preccurlyeq \mathrm{\omega }$$
7		breq1	$$⊢A=\left(1..^M\right)\to \left(A\preccurlyeq \mathrm{\omega }\leftrightarrow \left(1..^M\right)\preccurlyeq \mathrm{\omega }\right)$$
8	6 7	mpbiri	$$⊢A=\left(1..^M\right)\to A\preccurlyeq \mathrm{\omega }$$
9	3 8	jaoi	$$⊢\left(A=\mathbb{N}\vee A=\left(1..^M\right)\right)\to A\preccurlyeq \mathrm{\omega }$$