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 ⊢ C ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uzsuci ⊢ A ∈ ω → G ⁡ suc ⁡ A = G ⁡ A + 1

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ C ∈ ℤ
2 om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
3 suceq ⊢ z = A → suc ⁡ z = suc ⁡ A
4 3 fveq2d ⊢ z = A → G ⁡ suc ⁡ z = G ⁡ suc ⁡ A
5 fveq2 ⊢ z = A → G ⁡ z = G ⁡ A
6 5 oveq1d ⊢ z = A → G ⁡ z + 1 = G ⁡ A + 1
7 4 6 eqeq12d ⊢ z = A → G ⁡ suc ⁡ z = G ⁡ z + 1 ↔ G ⁡ suc ⁡ A = G ⁡ A + 1
8 ovex ⊢ G ⁡ z + 1 ∈ V
9 oveq1 ⊢ y = x → y + 1 = x + 1
10 oveq1 ⊢ y = G ⁡ z → y + 1 = G ⁡ z + 1
11 2 9 10 frsucmpt2 ⊢ z ∈ ω ∧ G ⁡ z + 1 ∈ V → G ⁡ suc ⁡ z = G ⁡ z + 1
12 8 11 mpan2 ⊢ z ∈ ω → G ⁡ suc ⁡ z = G ⁡ z + 1
13 7 12 vtoclga ⊢ A ∈ ω → G ⁡ suc ⁡ A = G ⁡ A + 1