Metamath Proof Explorer

Theorem om2uzrani

Description: Range of G (see om2uz0i ). (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 ⊢ C ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uzrani ⊢ ran ⁡ G = ℤ ≥ C

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ C ∈ ℤ
2 om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
3 frfnom ⊢ rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω Fn ω
4 2 fneq1i ⊢ G Fn ω ↔ rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω Fn ω
5 3 4 mpbir ⊢ G Fn ω
6 fvelrnb ⊢ G Fn ω → y ∈ ran ⁡ G ↔ ∃ z ∈ ω G ⁡ z = y
7 5 6 ax-mp ⊢ y ∈ ran ⁡ G ↔ ∃ z ∈ ω G ⁡ z = y
8 1 2 om2uzuzi ⊢ z ∈ ω → G ⁡ z ∈ ℤ ≥ C
9 eleq1 ⊢ G ⁡ z = y → G ⁡ z ∈ ℤ ≥ C ↔ y ∈ ℤ ≥ C
10 8 9 syl5ibcom ⊢ z ∈ ω → G ⁡ z = y → y ∈ ℤ ≥ C
11 10 rexlimiv ⊢ ∃ z ∈ ω G ⁡ z = y → y ∈ ℤ ≥ C
12 7 11 sylbi ⊢ y ∈ ran ⁡ G → y ∈ ℤ ≥ C
13 eleq1 ⊢ z = C → z ∈ ran ⁡ G ↔ C ∈ ran ⁡ G
14 eleq1 ⊢ z = y → z ∈ ran ⁡ G ↔ y ∈ ran ⁡ G
15 eleq1 ⊢ z = y + 1 → z ∈ ran ⁡ G ↔ y + 1 ∈ ran ⁡ G
16 1 2 om2uz0i ⊢ G ⁡ ∅ = C
17 peano1 ⊢ ∅ ∈ ω
18 fnfvelrn ⊢ G Fn ω ∧ ∅ ∈ ω → G ⁡ ∅ ∈ ran ⁡ G
19 5 17 18 mp2an ⊢ G ⁡ ∅ ∈ ran ⁡ G
20 16 19 eqeltrri ⊢ C ∈ ran ⁡ G
21 1 2 om2uzsuci ⊢ z ∈ ω → G ⁡ suc ⁡ z = G ⁡ z + 1
22 oveq1 ⊢ G ⁡ z = y → G ⁡ z + 1 = y + 1
23 21 22 sylan9eq ⊢ z ∈ ω ∧ G ⁡ z = y → G ⁡ suc ⁡ z = y + 1
24 peano2 ⊢ z ∈ ω → suc ⁡ z ∈ ω
25 fnfvelrn ⊢ G Fn ω ∧ suc ⁡ z ∈ ω → G ⁡ suc ⁡ z ∈ ran ⁡ G
26 5 24 25 sylancr ⊢ z ∈ ω → G ⁡ suc ⁡ z ∈ ran ⁡ G
27 26 adantr ⊢ z ∈ ω ∧ G ⁡ z = y → G ⁡ suc ⁡ z ∈ ran ⁡ G
28 23 27 eqeltrrd ⊢ z ∈ ω ∧ G ⁡ z = y → y + 1 ∈ ran ⁡ G
29 28 rexlimiva ⊢ ∃ z ∈ ω G ⁡ z = y → y + 1 ∈ ran ⁡ G
30 7 29 sylbi ⊢ y ∈ ran ⁡ G → y + 1 ∈ ran ⁡ G
31 30 a1i ⊢ y ∈ ℤ ≥ C → y ∈ ran ⁡ G → y + 1 ∈ ran ⁡ G
32 13 14 15 14 20 31 uzind4i ⊢ y ∈ ℤ ≥ C → y ∈ ran ⁡ G
33 12 32 impbii ⊢ y ∈ ran ⁡ G ↔ y ∈ ℤ ≥ C
34 33 eqriv ⊢ ran ⁡ G = ℤ ≥ C