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 ⊢ 𝐶 ∈ ℤ
om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion om2uzrani ran 𝐺 = ( ℤ≥ ‘ 𝐶 )

Proof

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