Theorem fz1nnct

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

	Ref	Expression
Assertion	fz1nnct	|- ( ( A = NN \/ A = ( 1 ..^ M ) ) -> A ~<_ _om )

Proof

Step	Hyp	Ref	Expression
1		nnct	|- NN ~<_ _om
2		breq1	|- ( A = NN -> ( A ~<_ _om <-> NN ~<_ _om ) )
3	1 2	mpbiri	|- ( A = NN -> A ~<_ _om )
4		fzofi	|- ( 1 ..^ M ) e. Fin
5		fict	|- ( ( 1 ..^ M ) e. Fin -> ( 1 ..^ M ) ~<_ _om )
6	4 5	ax-mp	|- ( 1 ..^ M ) ~<_ _om
7		breq1	|- ( A = ( 1 ..^ M ) -> ( A ~<_ _om <-> ( 1 ..^ M ) ~<_ _om ) )
8	6 7	mpbiri	|- ( A = ( 1 ..^ M ) -> A ~<_ _om )
9	3 8	jaoi	|- ( ( A = NN \/ A = ( 1 ..^ M ) ) -> A ~<_ _om )