Theorem uzct

Description: An upper integer set is countable. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	uzct.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
Assertion	uzct	⊢ 𝑍 ≼ ω

Proof

Step	Hyp	Ref	Expression
1		uzct.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑁 )
2		uzssz	⊢ ( ℤ≥ ‘ 𝑁 ) ⊆ ℤ
3	1 2	eqsstri	⊢ 𝑍 ⊆ ℤ
4		zex	⊢ ℤ ∈ V
5		ssdomg	⊢ ( ℤ ∈ V → ( 𝑍 ⊆ ℤ → 𝑍 ≼ ℤ ) )
6	4 5	ax-mp	⊢ ( 𝑍 ⊆ ℤ → 𝑍 ≼ ℤ )
7	3 6	ax-mp	⊢ 𝑍 ≼ ℤ
8		zct	⊢ ℤ ≼ ω
9		domtr	⊢ ( ( 𝑍 ≼ ℤ ∧ ℤ ≼ ω ) → 𝑍 ≼ ω )
10	7 8 9	mp2an	⊢ 𝑍 ≼ ω