This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝑍 ≼ ω