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	syl5ibr	⊢ ( 𝑧 ∈ ω → ( ( 𝐺 ‘ 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ suc 𝑧 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) )
19	4 6 8 10 14 18	finds	⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) )