Step | Hyp | Ref
| Expression |
1 | | seq3val.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑥 = 𝑀 → (𝐹‘𝑥) = (𝐹‘𝑀)) |
3 | 2 | eleq1d 2208 |
. . . . . . 7
⊢ (𝑥 = 𝑀 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑀) ∈ 𝑆)) |
4 | | seq3val.f |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
5 | 4 | ralrimiva 2505 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
6 | | uzid 9340 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
7 | 1, 6 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
8 | 3, 5, 7 | rspcdva 2794 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝑆) |
9 | | ssv 3119 |
. . . . . . 7
⊢ 𝑆 ⊆ V |
10 | 9 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ V) |
11 | | seq3val.pl |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
12 | 4, 11 | iseqovex 10229 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝑆) |
13 | | seq3val.r |
. . . . . 6
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) |
14 | 1, 8, 10, 12, 13 | frecuzrdgrclt 10188 |
. . . . 5
⊢ (𝜑 → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝑆)) |
15 | | ffn 5272 |
. . . . 5
⊢ (𝑅:ω⟶((ℤ≥‘𝑀) × 𝑆) → 𝑅 Fn ω) |
16 | 14, 15 | syl 14 |
. . . 4
⊢ (𝜑 → 𝑅 Fn ω) |
17 | | 1st2nd2 6073 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈
((ℤ≥‘𝑀) × 𝑆) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
18 | 17 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
19 | 18 | fveq2d 5425 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
20 | | df-ov 5777 |
. . . . . . . . . 10
⊢
((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉) |
21 | 19, 20 | syl6eqr 2190 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢))) |
22 | | xp1st 6063 |
. . . . . . . . . . 11
⊢ (𝑢 ∈
((ℤ≥‘𝑀) × 𝑆) → (1st ‘𝑢) ∈
(ℤ≥‘𝑀)) |
23 | 22 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (1st ‘𝑢) ∈
(ℤ≥‘𝑀)) |
24 | | xp2nd 6064 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈
((ℤ≥‘𝑀) × 𝑆) → (2nd ‘𝑢) ∈ 𝑆) |
25 | 24 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (2nd ‘𝑢) ∈ 𝑆) |
26 | 25 | elexd 2699 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (2nd ‘𝑢) ∈ V) |
27 | | peano2uz 9378 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑢) ∈ (ℤ≥‘𝑀) → ((1st
‘𝑢) + 1) ∈
(ℤ≥‘𝑀)) |
28 | 23, 27 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢) + 1) ∈
(ℤ≥‘𝑀)) |
29 | 11 | caovclg 5923 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆) |
30 | 29 | adantlr 468 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆) |
31 | | fveq2 5421 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((1st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1st ‘𝑢) + 1))) |
32 | 31 | eleq1d 2208 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((1st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝑆)) |
33 | 5 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
34 | 32, 33, 28 | rspcdva 2794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝑆) |
35 | 30, 25, 34 | caovcld 5924 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝑆) |
36 | | opelxpi 4571 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑢) + 1) ∈
(ℤ≥‘𝑀) ∧ ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝑆) → 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) + 1)))〉
∈ ((ℤ≥‘𝑀) × 𝑆)) |
37 | 28, 35, 36 | syl2anc 408 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) + 1)))〉
∈ ((ℤ≥‘𝑀) × 𝑆)) |
38 | | oveq1 5781 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑢) → (𝑥 + 1) = ((1st ‘𝑢) + 1)) |
39 | | fvoveq1 5797 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘𝑢) + 1))) |
40 | 39 | oveq2d 5790 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))) |
41 | 38, 40 | opeq12d 3713 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑢) → 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉 = 〈((1st
‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))〉) |
42 | | oveq1 5781 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘𝑢) → (𝑦 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
43 | 42 | opeq2d 3712 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑢) → 〈((1st
‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))〉 =
〈((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))〉) |
44 | | eqid 2139 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) |
45 | 41, 43, 44 | ovmpog 5905 |
. . . . . . . . . 10
⊢
(((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘𝑢) ∈ V ∧
〈((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) +
1)))〉) |
46 | 23, 26, 37, 45 | syl3anc 1216 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) +
1)))〉) |
47 | 21, 46 | eqtrd 2172 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) = 〈((1st ‘𝑢) + 1), ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))〉) |
48 | 47, 37 | eqeltrd 2216 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
49 | 48 | ralrimiva 2505 |
. . . . . 6
⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
50 | | opelxpi 4571 |
. . . . . . 7
⊢ ((𝑀 ∈
(ℤ≥‘𝑀) ∧ (𝐹‘𝑀) ∈ 𝑆) → 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
51 | 7, 8, 50 | syl2anc 408 |
. . . . . 6
⊢ (𝜑 → 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
52 | 49, 51 | jca 304 |
. . . . 5
⊢ (𝜑 → (∀𝑢 ∈
((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆))) |
53 | | frecfcl 6302 |
. . . . 5
⊢
((∀𝑢 ∈
((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆)) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉):ω⟶((ℤ≥‘𝑀) × 𝑆)) |
54 | | ffn 5272 |
. . . . 5
⊢
(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉):ω⟶((ℤ≥‘𝑀) × 𝑆) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦
∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) Fn ω) |
55 | 52, 53, 54 | 3syl 17 |
. . . 4
⊢ (𝜑 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) Fn ω) |
56 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅)) |
57 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = ∅ → (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅)) |
58 | 56, 57 | eqeq12d 2154 |
. . . . . . 7
⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅))) |
59 | 58 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅)))) |
60 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘)) |
61 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) |
62 | 60, 61 | eqeq12d 2154 |
. . . . . . 7
⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
63 | 62 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)))) |
64 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘)) |
65 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)) |
66 | 64, 65 | eqeq12d 2154 |
. . . . . . 7
⊢ (𝑐 = suc 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘))) |
67 | 66 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = suc 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)))) |
68 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛)) |
69 | | fveq2 5421 |
. . . . . . . 8
⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛)) |
70 | 68, 69 | eqeq12d 2154 |
. . . . . . 7
⊢ (𝑐 = 𝑛 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛))) |
71 | 70 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = 𝑛 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛)))) |
72 | 13 | fveq1i 5422 |
. . . . . . . 8
⊢ (𝑅‘∅) = (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) |
73 | | frec0g 6294 |
. . . . . . . . 9
⊢
(〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
74 | 51, 73 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
75 | 72, 74 | syl5eq 2184 |
. . . . . . 7
⊢ (𝜑 → (𝑅‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
76 | | frec0g 6294 |
. . . . . . . 8
⊢
(〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
77 | 51, 76 | syl 14 |
. . . . . . 7
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
78 | 75, 77 | eqtr4d 2175 |
. . . . . 6
⊢ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅)) |
79 | 14 | ad2antlr 480 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝑆)) |
80 | | simpll 518 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 𝑘 ∈ ω) |
81 | 79, 80 | ffvelrnd 5556 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
82 | | xp1st 6063 |
. . . . . . . . . . 11
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀)) |
83 | 81, 82 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀)) |
84 | | xp2nd 6064 |
. . . . . . . . . . . 12
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑆) |
85 | 81, 84 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝑆) |
86 | 85 | elexd 2699 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ V) |
87 | 29 | adantll 467 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆) |
88 | 87 | adantlr 468 |
. . . . . . . . . . . . . 14
⊢ ((((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆) |
89 | | fveq2 5421 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = ((1st
‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) |
90 | 89 | eleq1d 2208 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = ((1st
‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝑆 ↔ (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝑆)) |
91 | | fveq2 5421 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
92 | 91 | eleq1d 2208 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑎) ∈ 𝑆)) |
93 | 92 | cbvralv 2654 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑥 ∈
(ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆 ↔ ∀𝑎 ∈ (ℤ≥‘𝑀)(𝐹‘𝑎) ∈ 𝑆) |
94 | 5, 93 | sylib 121 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑎 ∈ (ℤ≥‘𝑀)(𝐹‘𝑎) ∈ 𝑆) |
95 | 94 | ad2antlr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑎 ∈ (ℤ≥‘𝑀)(𝐹‘𝑎) ∈ 𝑆) |
96 | | peano2uz 9378 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) → ((1st
‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘𝑀)) |
97 | 83, 96 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘𝑀)) |
98 | 90, 95, 97 | rspcdva 2794 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝑆) |
99 | 88, 85, 98 | caovcld 5924 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝑆) |
100 | | fvoveq1 5797 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) |
101 | 100 | oveq2d 5790 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
102 | | oveq1 5781 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (2nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
103 | | eqid 2139 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) |
104 | 101, 102,
103 | ovmpog 5905 |
. . . . . . . . . . . . 13
⊢
(((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘(𝑅‘𝑘)) ∈ 𝑆 ∧ ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝑆) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
105 | 83, 85, 99, 104 | syl3anc 1216 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
106 | 105 | opeq2d 3712 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((2nd
‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
107 | 105, 99 | eqeltrd 2216 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) ∈ 𝑆) |
108 | | opelxpi 4571 |
. . . . . . . . . . . 12
⊢
((((1st ‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘𝑀) ∧ ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) ∈ 𝑆) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
109 | 97, 107, 108 | syl2anc 408 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
110 | 106, 109 | eqeltrrd 2217 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((2nd
‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
111 | | oveq1 5781 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1st ‘(𝑅‘𝑘)) + 1)) |
112 | | fvoveq1 5797 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) |
113 | 112 | oveq2d 5790 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
114 | 111, 113 | opeq12d 3713 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
115 | | oveq1 5781 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
116 | 115 | opeq2d 3712 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((2nd
‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
117 | 114, 116,
44 | ovmpog 5905 |
. . . . . . . . . 10
⊢
(((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘(𝑅‘𝑘)) ∈ V ∧
〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
118 | 83, 86, 110, 117 | syl3anc 1216 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
119 | 49 | ad2antlr 480 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
120 | 51 | ad2antlr 480 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
121 | | frecsuc 6304 |
. . . . . . . . . . . 12
⊢
((∀𝑢 ∈
((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
122 | 119, 120,
80, 121 | syl3anc 1216 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
123 | | simpr 109 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) |
124 | 123 | fveq2d 5425 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
125 | 122, 124 | eqtr4d 2175 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘))) |
126 | | 1st2nd2 6073 |
. . . . . . . . . . . . 13
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝑆) → (𝑅‘𝑘) = 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉) |
127 | 81, 126 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘𝑘) = 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉) |
128 | 127 | fveq2d 5425 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
129 | | df-ov 5777 |
. . . . . . . . . . 11
⊢
((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉) |
130 | 128, 129 | syl6eqr 2190 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘)) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘)))) |
131 | 125, 130 | eqtrd 2172 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘)))) |
132 | 13 | fveq1i 5422 |
. . . . . . . . . . . . . . 15
⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) |
133 | 18 | fveq2d 5425 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
134 | | df-ov 5777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉) |
135 | 133, 134 | syl6eqr 2190 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢))) |
136 | | fvoveq1 5797 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = (1st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘𝑢) + 1))) |
137 | 136 | oveq2d 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = (1st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘𝑢) + 1)))) |
138 | | oveq1 5781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = (2nd ‘𝑢) → (𝑤 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
139 | 137, 138,
103 | ovmpog 5905 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘𝑢) ∈ 𝑆 ∧ ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) + 1))) ∈
𝑆) → ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
140 | 23, 25, 35, 139 | syl3anc 1216 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
141 | 140, 35 | eqeltrd 2216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) ∈ 𝑆) |
142 | | opelxpi 4571 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((1st ‘𝑢) + 1) ∈
(ℤ≥‘𝑀) ∧ ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) ∈ 𝑆) → 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
143 | 28, 141, 142 | syl2anc 408 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) |
144 | | oveq1 5781 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = (1st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)) |
145 | 38, 144 | opeq12d 3713 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = (1st ‘𝑢) → 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) |
146 | | oveq2 5782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (2nd ‘𝑢) → ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))) |
147 | 146 | opeq2d 3712 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (2nd ‘𝑢) → 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
148 | | eqid 2139 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) |
149 | 145, 147,
148 | ovmpog 5905 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘𝑢) ∈ V ∧
〈((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
150 | 23, 26, 143, 149 | syl3anc 1216 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
151 | 135, 150 | eqtrd 2172 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) = 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
152 | 151, 143 | eqeltrd 2216 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
153 | 152 | ralrimiva 2505 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
154 | 153 | ad2antlr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆)) |
155 | | frecsuc 6304 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑢 ∈
((ℤ≥‘𝑀) × 𝑆)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝑆) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝑆) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
156 | 154, 120,
80, 155 | syl3anc 1216 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
157 | 132, 156 | syl5eq 2184 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
158 | 13 | fveq1i 5422 |
. . . . . . . . . . . . . . 15
⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘) |
159 | 158 | fveq2i 5424 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) |
160 | 157, 159 | syl6eqr 2190 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(𝑅‘𝑘))) |
161 | 127 | fveq2d 5425 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
162 | 160, 161 | eqtrd 2172 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
163 | | df-ov 5777 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉) |
164 | 162, 163 | syl6eqr 2190 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘)))) |
165 | | oveq1 5781 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)) |
166 | 111, 165 | opeq12d 3713 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) |
167 | | oveq2 5782 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))) |
168 | 167 | opeq2d 3712 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
169 | 166, 168,
148 | ovmpog 5905 |
. . . . . . . . . . . 12
⊢
(((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘(𝑅‘𝑘)) ∈ V ∧
〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝑀) × 𝑆)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
170 | 83, 86, 109, 169 | syl3anc 1216 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
171 | 164, 170 | eqtrd 2172 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
172 | 171, 106 | eqtrd 2172 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
173 | 118, 131,
172 | 3eqtr4rd 2183 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)) |
174 | 173 | exp31 361 |
. . . . . . 7
⊢ (𝑘 ∈ ω → (𝜑 → ((𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)))) |
175 | 174 | a2d 26 |
. . . . . 6
⊢ (𝑘 ∈ ω → ((𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)))) |
176 | 59, 63, 67, 71, 78, 175 | finds 4514 |
. . . . 5
⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛))) |
177 | 176 | impcom 124 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛)) |
178 | 16, 55, 177 | eqfnfvd 5521 |
. . 3
⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
179 | 178 | rneqd 4768 |
. 2
⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
180 | | df-seqfrec 10219 |
. 2
⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) |
181 | 179, 180 | syl6reqr 2191 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅) |