Metamath Proof Explorer


Theorem om2uzrdg

Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0 ) with characteristic function F ( x , y ) and initial value A . Normally F is a function on the partition, and A is a member of the partition. See also comment in om2uz0i . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 18-Nov-2014)

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

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 fveq2 ( 𝑧 = ∅ → ( 𝑅𝑧 ) = ( 𝑅 ‘ ∅ ) )
6 fveq2 ( 𝑧 = ∅ → ( 𝐺𝑧 ) = ( 𝐺 ‘ ∅ ) )
7 2fveq3 ( 𝑧 = ∅ → ( 2nd ‘ ( 𝑅𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) )
8 6 7 opeq12d ( 𝑧 = ∅ → ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ )
9 5 8 eqeq12d ( 𝑧 = ∅ → ( ( 𝑅𝑧 ) = ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ ) )
10 fveq2 ( 𝑧 = 𝑣 → ( 𝑅𝑧 ) = ( 𝑅𝑣 ) )
11 fveq2 ( 𝑧 = 𝑣 → ( 𝐺𝑧 ) = ( 𝐺𝑣 ) )
12 2fveq3 ( 𝑧 = 𝑣 → ( 2nd ‘ ( 𝑅𝑧 ) ) = ( 2nd ‘ ( 𝑅𝑣 ) ) )
13 11 12 opeq12d ( 𝑧 = 𝑣 → ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ )
14 10 13 eqeq12d ( 𝑧 = 𝑣 → ( ( 𝑅𝑧 ) = ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ ↔ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) )
15 fveq2 ( 𝑧 = suc 𝑣 → ( 𝑅𝑧 ) = ( 𝑅 ‘ suc 𝑣 ) )
16 fveq2 ( 𝑧 = suc 𝑣 → ( 𝐺𝑧 ) = ( 𝐺 ‘ suc 𝑣 ) )
17 2fveq3 ( 𝑧 = suc 𝑣 → ( 2nd ‘ ( 𝑅𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) )
18 16 17 opeq12d ( 𝑧 = suc 𝑣 → ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ )
19 15 18 eqeq12d ( 𝑧 = suc 𝑣 → ( ( 𝑅𝑧 ) = ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) )
20 fveq2 ( 𝑧 = 𝐵 → ( 𝑅𝑧 ) = ( 𝑅𝐵 ) )
21 fveq2 ( 𝑧 = 𝐵 → ( 𝐺𝑧 ) = ( 𝐺𝐵 ) )
22 2fveq3 ( 𝑧 = 𝐵 → ( 2nd ‘ ( 𝑅𝑧 ) ) = ( 2nd ‘ ( 𝑅𝐵 ) ) )
23 21 22 opeq12d ( 𝑧 = 𝐵 → ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ = ⟨ ( 𝐺𝐵 ) , ( 2nd ‘ ( 𝑅𝐵 ) ) ⟩ )
24 20 23 eqeq12d ( 𝑧 = 𝐵 → ( ( 𝑅𝑧 ) = ⟨ ( 𝐺𝑧 ) , ( 2nd ‘ ( 𝑅𝑧 ) ) ⟩ ↔ ( 𝑅𝐵 ) = ⟨ ( 𝐺𝐵 ) , ( 2nd ‘ ( 𝑅𝐵 ) ) ⟩ ) )
25 4 fveq1i ( 𝑅 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ )
26 opex 𝐶 , 𝐴 ⟩ ∈ V
27 fr0g ( ⟨ 𝐶 , 𝐴 ⟩ ∈ V → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩ )
28 26 27 ax-mp ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴
29 25 28 eqtri ( 𝑅 ‘ ∅ ) = ⟨ 𝐶 , 𝐴
30 1 2 om2uz0i ( 𝐺 ‘ ∅ ) = 𝐶
31 29 fveq2i ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) = ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ )
32 1 elexi 𝐶 ∈ V
33 32 3 op2nd ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ ) = 𝐴
34 31 33 eqtri ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) = 𝐴
35 30 34 opeq12i ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ = ⟨ 𝐶 , 𝐴
36 29 35 eqtr4i ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩
37 frsuc ( 𝑣 ∈ ω → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) ) )
38 4 fveq1i ( 𝑅 ‘ suc 𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 )
39 4 fveq1i ( 𝑅𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 )
40 39 fveq2i ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) )
41 37 38 40 3eqtr4g ( 𝑣 ∈ ω → ( 𝑅 ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅𝑣 ) ) )
42 fveq2 ( ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) )
43 df-ov ( ( 𝐺𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅𝑣 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ )
44 fvex ( 𝐺𝑣 ) ∈ V
45 fvex ( 2nd ‘ ( 𝑅𝑣 ) ) ∈ V
46 oveq1 ( 𝑤 = ( 𝐺𝑣 ) → ( 𝑤 + 1 ) = ( ( 𝐺𝑣 ) + 1 ) )
47 oveq1 ( 𝑤 = ( 𝐺𝑣 ) → ( 𝑤 𝐹 𝑧 ) = ( ( 𝐺𝑣 ) 𝐹 𝑧 ) )
48 46 47 opeq12d ( 𝑤 = ( 𝐺𝑣 ) → ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑧 ) ⟩ = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 𝑧 ) ⟩ )
49 oveq2 ( 𝑧 = ( 2nd ‘ ( 𝑅𝑣 ) ) → ( ( 𝐺𝑣 ) 𝐹 𝑧 ) = ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) )
50 49 opeq2d ( 𝑧 = ( 2nd ‘ ( 𝑅𝑣 ) ) → ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 𝑧 ) ⟩ = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ )
51 oveq1 ( 𝑥 = 𝑤 → ( 𝑥 + 1 ) = ( 𝑤 + 1 ) )
52 oveq1 ( 𝑥 = 𝑤 → ( 𝑥 𝐹 𝑦 ) = ( 𝑤 𝐹 𝑦 ) )
53 51 52 opeq12d ( 𝑥 = 𝑤 → ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑦 ) ⟩ )
54 oveq2 ( 𝑦 = 𝑧 → ( 𝑤 𝐹 𝑦 ) = ( 𝑤 𝐹 𝑧 ) )
55 54 opeq2d ( 𝑦 = 𝑧 → ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑧 ) ⟩ )
56 53 55 cbvmpov ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) = ( 𝑤 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑧 ) ⟩ )
57 opex ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ ∈ V
58 48 50 56 57 ovmpo ( ( ( 𝐺𝑣 ) ∈ V ∧ ( 2nd ‘ ( 𝑅𝑣 ) ) ∈ V ) → ( ( 𝐺𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅𝑣 ) ) ) = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ )
59 44 45 58 mp2an ( ( 𝐺𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅𝑣 ) ) ) = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩
60 43 59 eqtr3i ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩
61 42 60 eqtrdi ( ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅𝑣 ) ) = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ )
62 41 61 sylan9eq ( ( 𝑣 ∈ ω ∧ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ )
63 1 2 om2uzsuci ( 𝑣 ∈ ω → ( 𝐺 ‘ suc 𝑣 ) = ( ( 𝐺𝑣 ) + 1 ) )
64 63 adantr ( ( 𝑣 ∈ ω ∧ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) → ( 𝐺 ‘ suc 𝑣 ) = ( ( 𝐺𝑣 ) + 1 ) )
65 62 fveq2d ( ( 𝑣 ∈ ω ∧ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) → ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) = ( 2nd ‘ ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ ) )
66 ovex ( ( 𝐺𝑣 ) + 1 ) ∈ V
67 ovex ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ∈ V
68 66 67 op2nd ( 2nd ‘ ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ ) = ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) )
69 65 68 eqtrdi ( ( 𝑣 ∈ ω ∧ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) → ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) = ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) )
70 64 69 opeq12d ( ( 𝑣 ∈ ω ∧ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) → ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ = ⟨ ( ( 𝐺𝑣 ) + 1 ) , ( ( 𝐺𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅𝑣 ) ) ) ⟩ )
71 62 70 eqtr4d ( ( 𝑣 ∈ ω ∧ ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ ) → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ )
72 71 ex ( 𝑣 ∈ ω → ( ( 𝑅𝑣 ) = ⟨ ( 𝐺𝑣 ) , ( 2nd ‘ ( 𝑅𝑣 ) ) ⟩ → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) )
73 9 14 19 24 36 72 finds ( 𝐵 ∈ ω → ( 𝑅𝐵 ) = ⟨ ( 𝐺𝐵 ) , ( 2nd ‘ ( 𝑅𝐵 ) ) ⟩ )