Metamath Proof Explorer


Theorem uzrdgsuci

Description: Successor value of a recursive definition generator on upper integers. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 𝐶 ∈ ℤ
om2uz.2 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
uzrdg.1 𝐴 ∈ V
uzrdg.2 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
uzrdg.3 𝑆 = ran 𝑅
Assertion uzrdgsuci ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 𝐵 𝐹 ( 𝑆𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 𝐶 ∈ ℤ
2 om2uz.2 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3 uzrdg.1 𝐴 ∈ V
4 uzrdg.2 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
5 uzrdg.3 𝑆 = ran 𝑅
6 1 2 3 4 5 uzrdgfni 𝑆 Fn ( ℤ𝐶 )
7 fnfun ( 𝑆 Fn ( ℤ𝐶 ) → Fun 𝑆 )
8 6 7 ax-mp Fun 𝑆
9 peano2uz ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝐵 + 1 ) ∈ ( ℤ𝐶 ) )
10 1 2 3 4 uzrdglem ( ( 𝐵 + 1 ) ∈ ( ℤ𝐶 ) → ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ ran 𝑅 )
11 9 10 syl ( 𝐵 ∈ ( ℤ𝐶 ) → ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ ran 𝑅 )
12 11 5 eleqtrrdi ( 𝐵 ∈ ( ℤ𝐶 ) → ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ 𝑆 )
13 funopfv ( Fun 𝑆 → ( ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ 𝑆 → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ) )
14 8 12 13 mpsyl ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) )
15 1 2 om2uzf1oi 𝐺 : ω –1-1-onto→ ( ℤ𝐶 )
16 f1ocnvdm ( ( 𝐺 : ω –1-1-onto→ ( ℤ𝐶 ) ∧ 𝐵 ∈ ( ℤ𝐶 ) ) → ( 𝐺𝐵 ) ∈ ω )
17 15 16 mpan ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝐺𝐵 ) ∈ ω )
18 peano2 ( ( 𝐺𝐵 ) ∈ ω → suc ( 𝐺𝐵 ) ∈ ω )
19 17 18 syl ( 𝐵 ∈ ( ℤ𝐶 ) → suc ( 𝐺𝐵 ) ∈ ω )
20 1 2 om2uzsuci ( ( 𝐺𝐵 ) ∈ ω → ( 𝐺 ‘ suc ( 𝐺𝐵 ) ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) )
21 17 20 syl ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝐺 ‘ suc ( 𝐺𝐵 ) ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) )
22 f1ocnvfv2 ( ( 𝐺 : ω –1-1-onto→ ( ℤ𝐶 ) ∧ 𝐵 ∈ ( ℤ𝐶 ) ) → ( 𝐺 ‘ ( 𝐺𝐵 ) ) = 𝐵 )
23 15 22 mpan ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝐺 ‘ ( 𝐺𝐵 ) ) = 𝐵 )
24 23 oveq1d ( 𝐵 ∈ ( ℤ𝐶 ) → ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) = ( 𝐵 + 1 ) )
25 21 24 eqtrd ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝐺 ‘ suc ( 𝐺𝐵 ) ) = ( 𝐵 + 1 ) )
26 f1ocnvfv ( ( 𝐺 : ω –1-1-onto→ ( ℤ𝐶 ) ∧ suc ( 𝐺𝐵 ) ∈ ω ) → ( ( 𝐺 ‘ suc ( 𝐺𝐵 ) ) = ( 𝐵 + 1 ) → ( 𝐺 ‘ ( 𝐵 + 1 ) ) = suc ( 𝐺𝐵 ) ) )
27 15 26 mpan ( suc ( 𝐺𝐵 ) ∈ ω → ( ( 𝐺 ‘ suc ( 𝐺𝐵 ) ) = ( 𝐵 + 1 ) → ( 𝐺 ‘ ( 𝐵 + 1 ) ) = suc ( 𝐺𝐵 ) ) )
28 19 25 27 sylc ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝐺 ‘ ( 𝐵 + 1 ) ) = suc ( 𝐺𝐵 ) )
29 28 fveq2d ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) = ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) )
30 29 fveq2d ( 𝐵 ∈ ( ℤ𝐶 ) → ( 2nd ‘ ( 𝑅 ‘ ( 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) = ( 2nd ‘ ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) ) )
31 14 30 eqtrd ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 2nd ‘ ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) ) )
32 frsuc ( ( 𝐺𝐵 ) ∈ ω → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( 𝐺𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( 𝐺𝐵 ) ) ) )
33 4 fveq1i ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( 𝐺𝐵 ) )
34 4 fveq1i ( 𝑅 ‘ ( 𝐺𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( 𝐺𝐵 ) )
35 34 fveq2i ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( 𝐺𝐵 ) ) )
36 32 33 35 3eqtr4g ( ( 𝐺𝐵 ) ∈ ω → ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) )
37 1 2 3 4 om2uzrdg ( ( 𝐺𝐵 ) ∈ ω → ( 𝑅 ‘ ( 𝐺𝐵 ) ) = ⟨ ( 𝐺 ‘ ( 𝐺𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ⟩ )
38 37 fveq2d ( ( 𝐺𝐵 ) ∈ ω → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ ( 𝐺𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ⟩ ) )
39 df-ov ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ ( 𝐺𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ⟩ )
40 38 39 eqtr4di ( ( 𝐺𝐵 ) ∈ ω → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) )
41 36 40 eqtrd ( ( 𝐺𝐵 ) ∈ ω → ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) )
42 fvex ( 𝐺 ‘ ( 𝐺𝐵 ) ) ∈ V
43 fvex ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ∈ V
44 oveq1 ( 𝑧 = ( 𝐺 ‘ ( 𝐺𝐵 ) ) → ( 𝑧 + 1 ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) )
45 oveq1 ( 𝑧 = ( 𝐺 ‘ ( 𝐺𝐵 ) ) → ( 𝑧 𝐹 𝑤 ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 𝑤 ) )
46 44 45 opeq12d ( 𝑧 = ( 𝐺 ‘ ( 𝐺𝐵 ) ) → ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑤 ) ⟩ = ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 𝑤 ) ⟩ )
47 oveq2 ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) → ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 𝑤 ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) )
48 47 opeq2d ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) → ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 𝑤 ) ⟩ = ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩ )
49 oveq1 ( 𝑥 = 𝑧 → ( 𝑥 + 1 ) = ( 𝑧 + 1 ) )
50 oveq1 ( 𝑥 = 𝑧 → ( 𝑥 𝐹 𝑦 ) = ( 𝑧 𝐹 𝑦 ) )
51 49 50 opeq12d ( 𝑥 = 𝑧 → ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑦 ) ⟩ )
52 oveq2 ( 𝑦 = 𝑤 → ( 𝑧 𝐹 𝑦 ) = ( 𝑧 𝐹 𝑤 ) )
53 52 opeq2d ( 𝑦 = 𝑤 → ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑤 ) ⟩ )
54 51 53 cbvmpov ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) = ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑤 ) ⟩ )
55 opex ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩ ∈ V
56 46 48 54 55 ovmpo ( ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) ∈ V ∧ ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ∈ V ) → ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) = ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩ )
57 42 43 56 mp2an ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) = ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩
58 41 57 eqtrdi ( ( 𝐺𝐵 ) ∈ ω → ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) = ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩ )
59 58 fveq2d ( ( 𝐺𝐵 ) ∈ ω → ( 2nd ‘ ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) ) = ( 2nd ‘ ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩ ) )
60 ovex ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) ∈ V
61 ovex ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ∈ V
62 60 61 op2nd ( 2nd ‘ ⟨ ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) ⟩ ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) )
63 59 62 eqtrdi ( ( 𝐺𝐵 ) ∈ ω → ( 2nd ‘ ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) )
64 17 63 syl ( 𝐵 ∈ ( ℤ𝐶 ) → ( 2nd ‘ ( 𝑅 ‘ suc ( 𝐺𝐵 ) ) ) = ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) )
65 1 2 3 4 uzrdglem ( 𝐵 ∈ ( ℤ𝐶 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ⟩ ∈ ran 𝑅 )
66 65 5 eleqtrrdi ( 𝐵 ∈ ( ℤ𝐶 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ⟩ ∈ 𝑆 )
67 funopfv ( Fun 𝑆 → ( ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ⟩ ∈ 𝑆 → ( 𝑆𝐵 ) = ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) )
68 8 66 67 mpsyl ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝑆𝐵 ) = ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) )
69 68 eqcomd ( 𝐵 ∈ ( ℤ𝐶 ) → ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) = ( 𝑆𝐵 ) )
70 23 69 oveq12d ( 𝐵 ∈ ( ℤ𝐶 ) → ( ( 𝐺 ‘ ( 𝐺𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( 𝐺𝐵 ) ) ) ) = ( 𝐵 𝐹 ( 𝑆𝐵 ) ) )
71 31 64 70 3eqtrd ( 𝐵 ∈ ( ℤ𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 𝐵 𝐹 ( 𝑆𝐵 ) ) )