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 = if M ∈ ℤ M 0 → ℤ ≥ M = ℤ ≥ if M ∈ ℤ M 0
3 1 2 eqtrid ⊢ M = if M ∈ ℤ M 0 → Z = ℤ ≥ if M ∈ ℤ M 0
4 3 breq1d ⊢ M = if M ∈ ℤ M 0 → Z ≈ ω ↔ ℤ ≥ if M ∈ ℤ M 0 ≈ ω
5 omex ⊢ ω ∈ V
6 fvex ⊢ ℤ ≥ if M ∈ ℤ M 0 ∈ V
7 0z ⊢ 0 ∈ ℤ
8 7 elimel ⊢ if M ∈ ℤ M 0 ∈ ℤ
9 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω
10 8 9 om2uzf1oi ⊢ rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω : ω ⟶ 1-1 onto ℤ ≥ if M ∈ ℤ M 0
11 f1oen2g ⊢ ω ∈ V ∧ ℤ ≥ if M ∈ ℤ M 0 ∈ V ∧ rec ⁡ x ∈ V ⟼ x + 1 if M ∈ ℤ M 0 ↾ ω : ω ⟶ 1-1 onto ℤ ≥ if M ∈ ℤ M 0 → ω ≈ ℤ ≥ if M ∈ ℤ M 0
12 5 6 10 11 mp3an ⊢ ω ≈ ℤ ≥ if M ∈ ℤ M 0
13 12 ensymi ⊢ ℤ ≥ if M ∈ ℤ M 0 ≈ ω
14 4 13 dedth ⊢ M ∈ ℤ → Z ≈ ω