Theorem fz1nnct

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

	Ref	Expression
Assertion	fz1nnct	⊢ ( ( 𝐴 = ℕ ∨ 𝐴 = ( 1 ..^ 𝑀 ) ) → 𝐴 ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		nnct	⊢ ℕ ≼ ω
2		breq1	⊢ ( 𝐴 = ℕ → ( 𝐴 ≼ ω ↔ ℕ ≼ ω ) )
3	1 2	mpbiri	⊢ ( 𝐴 = ℕ → 𝐴 ≼ ω )
4		fzofi	⊢ ( 1 ..^ 𝑀 ) ∈ Fin
5		fict	⊢ ( ( 1 ..^ 𝑀 ) ∈ Fin → ( 1 ..^ 𝑀 ) ≼ ω )
6	4 5	ax-mp	⊢ ( 1 ..^ 𝑀 ) ≼ ω
7		breq1	⊢ ( 𝐴 = ( 1 ..^ 𝑀 ) → ( 𝐴 ≼ ω ↔ ( 1 ..^ 𝑀 ) ≼ ω ) )
8	6 7	mpbiri	⊢ ( 𝐴 = ( 1 ..^ 𝑀 ) → 𝐴 ≼ ω )
9	3 8	jaoi	⊢ ( ( 𝐴 = ℕ ∨ 𝐴 = ( 1 ..^ 𝑀 ) ) → 𝐴 ≼ ω )