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

Metamath Proof Explorer

Theorem om2uzuzi

Description: The value G (see om2uz0i ) at an ordinal natural number is in the upper integers. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 ⊢ 𝐶 ∈ ℤ
om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion om2uzuzi ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ 𝐶 ∈ ℤ
2 om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ∅ ) )
4 3 eleq1d ⊢ ( 𝑦 = ∅ → ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 ‘ ∅ ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
5 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑧 ) )
6 5 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 ‘ 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
7 fveq2 ⊢ ( 𝑦 = suc 𝑧 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ suc 𝑧 ) )
8 7 eleq1d ⊢ ( 𝑦 = suc 𝑧 → ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 ‘ suc 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
9 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝐴 ) )
10 9 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ↔ ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
11 1 2 om2uz0i ⊢ ( 𝐺 ‘ ∅ ) = 𝐶
12 uzid ⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ( ℤ≥ ‘ 𝐶 ) )
13 1 12 ax-mp ⊢ 𝐶 ∈ ( ℤ≥ ‘ 𝐶 )
14 11 13 eqeltri ⊢ ( 𝐺 ‘ ∅ ) ∈ ( ℤ≥ ‘ 𝐶 )
15 peano2uz ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( ( 𝐺 ‘ 𝑧 ) + 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
16 1 2 om2uzsuci ⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
17 16 eleq1d ⊢ ( 𝑧 ∈ ω → ( ( 𝐺 ‘ suc 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) ↔ ( ( 𝐺 ‘ 𝑧 ) + 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
18 15 17 imbitrrid ⊢ ( 𝑧 ∈ ω → ( ( 𝐺 ‘ 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ suc 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
19 4 6 8 10 14 18 finds ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) )