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

Metamath Proof Explorer

Theorem uzenom

Description: An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis uzinf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion uzenom ( 𝑀 ∈ ℤ → 𝑍 ≈ ω )

Proof

Step Hyp Ref Expression
1 uzinf.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 fveq2 ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
3 1 2 eqtrid ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → 𝑍 = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
4 3 breq1d ⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑍 ≈ ω ↔ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ≈ ω ) )
5 omex ⊢ ω ∈ V
6 fvex ⊢ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ∈ V
7 0z ⊢ 0 ∈ ℤ
8 7 elimel ⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
9 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω )
10 8 9 om2uzf1oi ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) : ω –1-1-onto→ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
11 f1oen2g ⊢ ( ( ω ∈ V ∧ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ∈ V ∧ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) : ω –1-1-onto→ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) → ω ≈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
12 5 6 10 11 mp3an ⊢ ω ≈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
13 12 ensymi ⊢ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ≈ ω
14 4 13 dedth ⊢ ( 𝑀 ∈ ℤ → 𝑍 ≈ ω )