Metamath Proof Explorer

Theorem uzenom

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

Ref Expression
Hypothesis uzinf.1 ⊢Z=ℤ≥M
Assertion uzenom ⊢M∈ℤ→Z≈ω

Proof

Step Hyp Ref Expression
1 uzinf.1 ⊢Z=ℤ≥M
2 fveq2 ⊢M=ifM∈ℤM0→ℤ≥M=ℤ≥ifM∈ℤM0
3 1 2 eqtrid ⊢M=ifM∈ℤM0→Z=ℤ≥ifM∈ℤM0
4 3 breq1d ⊢M=ifM∈ℤM0→Z≈ω↔ℤ≥ifM∈ℤM0≈ω
5 omex ⊢ω∈V
6 fvex ⊢ℤ≥ifM∈ℤM0∈V
7 0z ⊢0∈ℤ
8 7 elimel ⊢ifM∈ℤM0∈ℤ
9 eqid ⊢rec⁡x∈V⟼x+1ifM∈ℤM0↾ω=rec⁡x∈V⟼x+1ifM∈ℤM0↾ω
10 8 9 om2uzf1oi ⊢rec⁡x∈V⟼x+1ifM∈ℤM0↾ω:ω⟶1-1 ontoℤ≥ifM∈ℤM0
11 f1oen2g ⊢ω∈V∧ℤ≥ifM∈ℤM0∈V∧rec⁡x∈V⟼x+1ifM∈ℤM0↾ω:ω⟶1-1 ontoℤ≥ifM∈ℤM0→ω≈ℤ≥ifM∈ℤM0
12 5 6 10 11 mp3an ⊢ω≈ℤ≥ifM∈ℤM0
13 12 ensymi ⊢ℤ≥ifM∈ℤM0≈ω
14 4 13 dedth ⊢M∈ℤ→Z≈ω