Step | Hyp | Ref
| Expression |
1 | | uzrdg.b |
. 2
⊢ (𝜑 → 𝐵 ∈ ω) |
2 | | fveq2 5178 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝑅‘𝑧) = (𝑅‘𝐵)) |
3 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝐺‘𝑧) = (𝐺‘𝐵)) |
4 | 2 | fveq2d 5182 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝐵))) |
5 | 3, 4 | opeq12d 3557 |
. . . . 5
⊢ (𝑧 = 𝐵 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |
6 | 2, 5 | eqeq12d 2054 |
. . . 4
⊢ (𝑧 = 𝐵 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
7 | 6 | imbi2d 219 |
. . 3
⊢ (𝑧 = 𝐵 → ((𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉) ↔ (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉))) |
8 | | fveq2 5178 |
. . . . 5
⊢ (𝑧 = ∅ → (𝑅‘𝑧) = (𝑅‘∅)) |
9 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = ∅ → (𝐺‘𝑧) = (𝐺‘∅)) |
10 | 8 | fveq2d 5182 |
. . . . . 6
⊢ (𝑧 = ∅ →
(2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘∅))) |
11 | 9, 10 | opeq12d 3557 |
. . . . 5
⊢ (𝑧 = ∅ → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
12 | 8, 11 | eqeq12d 2054 |
. . . 4
⊢ (𝑧 = ∅ → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉)) |
13 | | fveq2 5178 |
. . . . 5
⊢ (𝑧 = 𝑣 → (𝑅‘𝑧) = (𝑅‘𝑣)) |
14 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (𝐺‘𝑧) = (𝐺‘𝑣)) |
15 | 13 | fveq2d 5182 |
. . . . . 6
⊢ (𝑧 = 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘𝑣))) |
16 | 14, 15 | opeq12d 3557 |
. . . . 5
⊢ (𝑧 = 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
17 | 13, 16 | eqeq12d 2054 |
. . . 4
⊢ (𝑧 = 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
18 | | fveq2 5178 |
. . . . 5
⊢ (𝑧 = suc 𝑣 → (𝑅‘𝑧) = (𝑅‘suc 𝑣)) |
19 | | fveq2 5178 |
. . . . . 6
⊢ (𝑧 = suc 𝑣 → (𝐺‘𝑧) = (𝐺‘suc 𝑣)) |
20 | 18 | fveq2d 5182 |
. . . . . 6
⊢ (𝑧 = suc 𝑣 → (2nd ‘(𝑅‘𝑧)) = (2nd ‘(𝑅‘suc 𝑣))) |
21 | 19, 20 | opeq12d 3557 |
. . . . 5
⊢ (𝑧 = suc 𝑣 → 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
22 | 18, 21 | eqeq12d 2054 |
. . . 4
⊢ (𝑧 = suc 𝑣 → ((𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉 ↔ (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
23 | | uzrdg.2 |
. . . . . . 7
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) |
24 | 23 | fveq1i 5179 |
. . . . . 6
⊢ (𝑅‘∅) = (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) |
25 | | frec2uz.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℤ) |
26 | | uzrdg.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
27 | | opexg 3964 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℤ ∧ 𝐴 ∈ 𝑆) → 〈𝐶, 𝐴〉 ∈ V) |
28 | 25, 26, 27 | syl2anc 391 |
. . . . . . 7
⊢ (𝜑 → 〈𝐶, 𝐴〉 ∈ V) |
29 | | frec0g 5983 |
. . . . . . 7
⊢
(〈𝐶, 𝐴〉 ∈ V →
(frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
30 | 28, 29 | syl 14 |
. . . . . 6
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘∅) = 〈𝐶, 𝐴〉) |
31 | 24, 30 | syl5eq 2084 |
. . . . 5
⊢ (𝜑 → (𝑅‘∅) = 〈𝐶, 𝐴〉) |
32 | | frec2uz.2 |
. . . . . . 7
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 𝐶) |
33 | 25, 32 | frec2uz0d 9185 |
. . . . . 6
⊢ (𝜑 → (𝐺‘∅) = 𝐶) |
34 | 31 | fveq2d 5182 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘(𝑅‘∅)) =
(2nd ‘〈𝐶, 𝐴〉)) |
35 | | uzid 8487 |
. . . . . . . . 9
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
(ℤ≥‘𝐶)) |
36 | 25, 35 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ (ℤ≥‘𝐶)) |
37 | | op2ndg 5778 |
. . . . . . . 8
⊢ ((𝐶 ∈
(ℤ≥‘𝐶) ∧ 𝐴 ∈ 𝑆) → (2nd ‘〈𝐶, 𝐴〉) = 𝐴) |
38 | 36, 26, 37 | syl2anc 391 |
. . . . . . 7
⊢ (𝜑 → (2nd
‘〈𝐶, 𝐴〉) = 𝐴) |
39 | 34, 38 | eqtrd 2072 |
. . . . . 6
⊢ (𝜑 → (2nd
‘(𝑅‘∅)) =
𝐴) |
40 | 33, 39 | opeq12d 3557 |
. . . . 5
⊢ (𝜑 → 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉 = 〈𝐶, 𝐴〉) |
41 | 31, 40 | eqtr4d 2075 |
. . . 4
⊢ (𝜑 → (𝑅‘∅) = 〈(𝐺‘∅), (2nd
‘(𝑅‘∅))〉) |
42 | | zex 8254 |
. . . . . . . . . . . . . . . 16
⊢ ℤ
∈ V |
43 | | uzssz 8492 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝐶) ⊆ ℤ |
44 | 42, 43 | ssexi 3895 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘𝐶) ∈ V |
45 | 44 | a1i 9 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ ω) →
(ℤ≥‘𝐶) ∈ V) |
46 | | uzrdg.s |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
47 | 46 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝑆 ∈ 𝑉) |
48 | | mpt2exga 5835 |
. . . . . . . . . . . . . 14
⊢
(((ℤ≥‘𝐶) ∈ V ∧ 𝑆 ∈ 𝑉) → (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V) |
49 | 45, 47, 48 | syl2anc 391 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V) |
50 | | vex 2560 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
51 | 50 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝑧 ∈ V) |
52 | | fvexg 5194 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
53 | 49, 51, 52 | syl2anc 391 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
54 | 53 | alrimiv 1754 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ∀𝑧((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V) |
55 | 28 | adantr 261 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 〈𝐶, 𝐴〉 ∈ V) |
56 | | simpr 103 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝑣 ∈ ω) |
57 | | frecsuc 5991 |
. . . . . . . . . . 11
⊢
((∀𝑧((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘𝑧) ∈ V ∧ 〈𝐶, 𝐴〉 ∈ V ∧ 𝑣 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣))) |
58 | 54, 55, 56, 57 | syl3anc 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣))) |
59 | 23 | fveq1i 5179 |
. . . . . . . . . 10
⊢ (𝑅‘suc 𝑣) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘suc 𝑣) |
60 | 23 | fveq1i 5179 |
. . . . . . . . . . 11
⊢ (𝑅‘𝑣) = (frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣) |
61 | 60 | fveq2i 5181 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉)‘𝑣)) |
62 | 58, 59, 61 | 3eqtr4g 2097 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑅‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
63 | 62 | adantr 261 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣))) |
64 | | fveq2 5178 |
. . . . . . . . 9
⊢ ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉)) |
65 | | df-ov 5515 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑣)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) |
66 | 25 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 𝐶 ∈ ℤ) |
67 | 66, 32, 56 | frec2uzuzd 9188 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘𝑣) ∈ (ℤ≥‘𝐶)) |
68 | | uzrdg.f |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝐶) ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
69 | 25, 32, 46, 26, 68, 23 | frecuzrdgrrn 9194 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝑅‘𝑣) ∈ ((ℤ≥‘𝐶) × 𝑆)) |
70 | | xp2nd 5793 |
. . . . . . . . . . . 12
⊢ ((𝑅‘𝑣) ∈ ((ℤ≥‘𝐶) × 𝑆) → (2nd ‘(𝑅‘𝑣)) ∈ 𝑆) |
71 | 69, 70 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (2nd
‘(𝑅‘𝑣)) ∈ 𝑆) |
72 | | peano2uz 8526 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑣) ∈ (ℤ≥‘𝐶) → ((𝐺‘𝑣) + 1) ∈
(ℤ≥‘𝐶)) |
73 | 67, 72 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣) + 1) ∈
(ℤ≥‘𝐶)) |
74 | 68 | caovclg 5653 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ (ℤ≥‘𝐶) ∧ 𝑤 ∈ 𝑆)) → (𝑧𝐹𝑤) ∈ 𝑆) |
75 | 74 | adantlr 446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑧 ∈ (ℤ≥‘𝐶) ∧ 𝑤 ∈ 𝑆)) → (𝑧𝐹𝑤) ∈ 𝑆) |
76 | 75, 67, 71 | caovcld 5654 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆) |
77 | | opelxp 4374 |
. . . . . . . . . . . 12
⊢
(〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈
((ℤ≥‘𝐶) × 𝑆) ↔ (((𝐺‘𝑣) + 1) ∈
(ℤ≥‘𝐶) ∧ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆)) |
78 | 73, 76, 77 | sylanbrc 394 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) |
79 | | oveq1 5519 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤 + 1) = ((𝐺‘𝑣) + 1)) |
80 | | oveq1 5519 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐺‘𝑣) → (𝑤𝐹𝑧) = ((𝐺‘𝑣)𝐹𝑧)) |
81 | 79, 80 | opeq12d 3557 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐺‘𝑣) → 〈(𝑤 + 1), (𝑤𝐹𝑧)〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)〉) |
82 | | oveq2 5520 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → ((𝐺‘𝑣)𝐹𝑧) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
83 | 82 | opeq2d 3556 |
. . . . . . . . . . . 12
⊢ (𝑧 = (2nd ‘(𝑅‘𝑣)) → 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹𝑧)〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
84 | | oveq1 5519 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥 + 1) = (𝑤 + 1)) |
85 | | oveq1 5519 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥𝐹𝑦) = (𝑤𝐹𝑦)) |
86 | 84, 85 | opeq12d 3557 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → 〈(𝑥 + 1), (𝑥𝐹𝑦)〉 = 〈(𝑤 + 1), (𝑤𝐹𝑦)〉) |
87 | | oveq2 5520 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (𝑤𝐹𝑦) = (𝑤𝐹𝑧)) |
88 | 87 | opeq2d 3556 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → 〈(𝑤 + 1), (𝑤𝐹𝑦)〉 = 〈(𝑤 + 1), (𝑤𝐹𝑧)〉) |
89 | 86, 88 | cbvmpt2v 5584 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉) = (𝑤 ∈ (ℤ≥‘𝐶), 𝑧 ∈ 𝑆 ↦ 〈(𝑤 + 1), (𝑤𝐹𝑧)〉) |
90 | 81, 83, 89 | ovmpt2g 5635 |
. . . . . . . . . . 11
⊢ (((𝐺‘𝑣) ∈ (ℤ≥‘𝐶) ∧ (2nd
‘(𝑅‘𝑣)) ∈ 𝑆 ∧ 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉 ∈
((ℤ≥‘𝐶) × 𝑆)) → ((𝐺‘𝑣)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
91 | 67, 71, 78, 90 | syl3anc 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣)(𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)(2nd ‘(𝑅‘𝑣))) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
92 | 65, 91 | syl5eqr 2086 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
93 | 64, 92 | sylan9eqr 2094 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → ((𝑥 ∈ (ℤ≥‘𝐶), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥𝐹𝑦)〉)‘(𝑅‘𝑣)) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
94 | 63, 93 | eqtrd 2072 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
95 | 66, 32, 56 | frec2uzsucd 9187 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
96 | 95 | adantr 261 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝐺‘suc 𝑣) = ((𝐺‘𝑣) + 1)) |
97 | 94 | fveq2d 5182 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘(𝑅‘suc 𝑣)) = (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉)) |
98 | 66, 32, 56 | frec2uzzd 9186 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (𝐺‘𝑣) ∈ ℤ) |
99 | 98 | peano2zd 8363 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝐺‘𝑣) + 1) ∈ ℤ) |
100 | 99 | adantr 261 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → ((𝐺‘𝑣) + 1) ∈ ℤ) |
101 | 76 | adantr 261 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆) |
102 | | op2ndg 5778 |
. . . . . . . . . 10
⊢ ((((𝐺‘𝑣) + 1) ∈ ℤ ∧ ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣))) ∈ 𝑆) → (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
103 | 100, 101,
102 | syl2anc 391 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
104 | 97, 103 | eqtrd 2072 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (2nd
‘(𝑅‘suc 𝑣)) = ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))) |
105 | 96, 104 | opeq12d 3557 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉 = 〈((𝐺‘𝑣) + 1), ((𝐺‘𝑣)𝐹(2nd ‘(𝑅‘𝑣)))〉) |
106 | 94, 105 | eqtr4d 2075 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑣 ∈ ω) ∧ (𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉) → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉) |
107 | 106 | ex 108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉)) |
108 | 107 | expcom 109 |
. . . 4
⊢ (𝑣 ∈ ω → (𝜑 → ((𝑅‘𝑣) = 〈(𝐺‘𝑣), (2nd ‘(𝑅‘𝑣))〉 → (𝑅‘suc 𝑣) = 〈(𝐺‘suc 𝑣), (2nd ‘(𝑅‘suc 𝑣))〉))) |
109 | 12, 17, 22, 41, 108 | finds2 4324 |
. . 3
⊢ (𝑧 ∈ ω → (𝜑 → (𝑅‘𝑧) = 〈(𝐺‘𝑧), (2nd ‘(𝑅‘𝑧))〉)) |
110 | 7, 109 | vtoclga 2619 |
. 2
⊢ (𝐵 ∈ ω → (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉)) |
111 | 1, 110 | mpcom 32 |
1
⊢ (𝜑 → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) |