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

Metamath Proof Explorer

Theorem om2uzsuci

Description: The value of G (see om2uz0i ) at a successor. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ 𝐶 ∈ ℤ
2 om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3 suceq ⊢ ( 𝑧 = 𝐴 → suc 𝑧 = suc 𝐴 )
4 3 fveq2d ⊢ ( 𝑧 = 𝐴 → ( 𝐺 ‘ suc 𝑧 ) = ( 𝐺 ‘ suc 𝐴 ) )
5 fveq2 ⊢ ( 𝑧 = 𝐴 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐴 ) )
6 5 oveq1d ⊢ ( 𝑧 = 𝐴 → ( ( 𝐺 ‘ 𝑧 ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) )
7 4 6 eqeq12d ⊢ ( 𝑧 = 𝐴 → ( ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) ↔ ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) ) )
8 ovex ⊢ ( ( 𝐺 ‘ 𝑧 ) + 1 ) ∈ V
9 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + 1 ) = ( 𝑥 + 1 ) )
10 oveq1 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝑦 + 1 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
11 2 9 10 frsucmpt2 ⊢ ( ( 𝑧 ∈ ω ∧ ( ( 𝐺 ‘ 𝑧 ) + 1 ) ∈ V ) → ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
12 8 11 mpan2 ⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
13 7 12 vtoclga ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) )