Step | Hyp | Ref
| Expression |
1 | | seqvalcd.m |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | seqvalcd.f0 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝑀) ∈ 𝐶) |
3 | | ssv 3085 |
. . . . . . 7
⊢ 𝐶 ⊆ V |
4 | 3 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 𝐶 ⊆ V) |
5 | | eqidd 2116 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))) |
6 | | simprr 504 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦) |
7 | | simprl 503 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → 𝑧 = 𝑥) |
8 | 7 | fvoveq1d 5750 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1))) |
9 | 6, 8 | oveq12d 5746 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) ∧ (𝑧 = 𝑥 ∧ 𝑤 = 𝑦)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
10 | | simprl 503 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
11 | | simprr 504 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
12 | | seqvalcd.pl |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)) → (𝑥 + 𝑦) ∈ 𝐶) |
13 | 12 | ralrimivva 2488 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶) |
14 | | oveq1 5735 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝑥 + 𝑦) = (𝑎 + 𝑦)) |
15 | 14 | eleq1d 2183 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → ((𝑥 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑦) ∈ 𝐶)) |
16 | | oveq2 5736 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → (𝑎 + 𝑦) = (𝑎 + 𝑏)) |
17 | 16 | eleq1d 2183 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑏 → ((𝑎 + 𝑦) ∈ 𝐶 ↔ (𝑎 + 𝑏) ∈ 𝐶)) |
18 | 15, 17 | cbvral2v 2636 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 ↔ ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶) |
19 | 13, 18 | sylib 121 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶) |
20 | 19 | adantr 272 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶) |
21 | | fveq2 5375 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑥 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑥 + 1))) |
22 | 21 | eleq1d 2183 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑥 + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝐷)) |
23 | | seqvalcd.fp1 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘(𝑀 + 1))) → (𝐹‘𝑥) ∈ 𝐷) |
24 | 23 | ralrimiva 2479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷) |
25 | | fveq2 5375 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
26 | 25 | eleq1d 2183 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘𝑎) ∈ 𝐷)) |
27 | 26 | cbvralv 2628 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷 ↔ ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
28 | 24, 27 | sylib 121 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
29 | 28 | adantr 272 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
30 | | eluzp1p1 9253 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝑥 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
31 | 10, 30 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
32 | 22, 29, 31 | rspcdva 2765 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(𝑥 + 1)) ∈ 𝐷) |
33 | | oveq12 5737 |
. . . . . . . . . . . 12
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → (𝑎 + 𝑏) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
34 | 33 | eleq1d 2183 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = (𝐹‘(𝑥 + 1))) → ((𝑎 + 𝑏) ∈ 𝐶 ↔ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)) |
35 | 34 | rspc2gv 2771 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐶 ∧ (𝐹‘(𝑥 + 1)) ∈ 𝐷) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)) |
36 | 11, 32, 35 | syl2anc 406 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (∀𝑎 ∈ 𝐶 ∀𝑏 ∈ 𝐷 (𝑎 + 𝑏) ∈ 𝐶 → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶)) |
37 | 20, 36 | mpd 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝐶) |
38 | 5, 9, 10, 11, 37 | ovmpod 5852 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
39 | 38, 37 | eqeltrd 2191 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝐶)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) ∈ 𝐶) |
40 | | seqvalcd.r |
. . . . . 6
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) |
41 | 1, 2, 4, 39, 40 | frecuzrdgrclt 10081 |
. . . . 5
⊢ (𝜑 → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝐶)) |
42 | 41 | ffnd 5231 |
. . . 4
⊢ (𝜑 → 𝑅 Fn ω) |
43 | | 1st2nd2 6027 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈
((ℤ≥‘𝑀) × 𝐶) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
44 | 43 | adantl 273 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → 𝑢 = 〈(1st ‘𝑢), (2nd ‘𝑢)〉) |
45 | 44 | fveq2d 5379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
46 | | df-ov 5731 |
. . . . . . . . . 10
⊢
((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉) |
47 | 45, 46 | syl6eqr 2165 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢))) |
48 | | xp1st 6017 |
. . . . . . . . . . 11
⊢ (𝑢 ∈
((ℤ≥‘𝑀) × 𝐶) → (1st ‘𝑢) ∈
(ℤ≥‘𝑀)) |
49 | 48 | adantl 273 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (1st ‘𝑢) ∈
(ℤ≥‘𝑀)) |
50 | | xp2nd 6018 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈
((ℤ≥‘𝑀) × 𝐶) → (2nd ‘𝑢) ∈ 𝐶) |
51 | 50 | adantl 273 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (2nd ‘𝑢) ∈ 𝐶) |
52 | 51 | elexd 2670 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (2nd ‘𝑢) ∈ V) |
53 | | peano2uz 9280 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑢) ∈ (ℤ≥‘𝑀) → ((1st
‘𝑢) + 1) ∈
(ℤ≥‘𝑀)) |
54 | 49, 53 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢) + 1) ∈
(ℤ≥‘𝑀)) |
55 | 13 | adantr 272 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶) |
56 | | fveq2 5375 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ((1st ‘𝑢) + 1) → (𝐹‘𝑥) = (𝐹‘((1st ‘𝑢) + 1))) |
57 | 56 | eleq1d 2183 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((1st ‘𝑢) + 1) → ((𝐹‘𝑥) ∈ 𝐷 ↔ (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝐷)) |
58 | 24 | adantr 272 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ∀𝑥 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑥) ∈ 𝐷) |
59 | | eluzp1p1 9253 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑢) ∈ (ℤ≥‘𝑀) → ((1st
‘𝑢) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
60 | 49, 59 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
61 | 57, 58, 60 | rspcdva 2765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝐷) |
62 | | oveq12 5737 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = (2nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1st ‘𝑢) + 1))) → (𝑥 + 𝑦) = ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))) |
63 | 62 | eleq1d 2183 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = (2nd ‘𝑢) ∧ 𝑦 = (𝐹‘((1st ‘𝑢) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶)) |
64 | 63 | rspc2gv 2771 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝑢) ∈ 𝐶 ∧ (𝐹‘((1st ‘𝑢) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶)) |
65 | 51, 61, 64 | syl2anc 406 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶)) |
66 | 55, 65 | mpd 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1))) ∈ 𝐶) |
67 | 54, 66 | opelxpd 4532 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) + 1)))〉
∈ ((ℤ≥‘𝑀) × 𝐶)) |
68 | | oveq1 5735 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑢) → (𝑥 + 1) = ((1st ‘𝑢) + 1)) |
69 | | fvoveq1 5751 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑢) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘𝑢) + 1))) |
70 | 69 | oveq2d 5744 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑢) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))) |
71 | 68, 70 | opeq12d 3679 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑢) → 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉 = 〈((1st
‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))〉) |
72 | | oveq1 5735 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘𝑢) → (𝑦 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
73 | 72 | opeq2d 3678 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑢) → 〈((1st
‘𝑢) + 1), (𝑦 + (𝐹‘((1st ‘𝑢) + 1)))〉 =
〈((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))〉) |
74 | | eqid 2115 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) |
75 | 71, 73, 74 | ovmpog 5859 |
. . . . . . . . . 10
⊢
(((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘𝑢) ∈ V ∧
〈((1st ‘𝑢) + 1), ((2nd ‘𝑢) + (𝐹‘((1st ‘𝑢) + 1)))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) +
1)))〉) |
76 | 49, 52, 67, 75 | syl3anc 1199 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((2nd ‘𝑢)
+ (𝐹‘((1st
‘𝑢) +
1)))〉) |
77 | 47, 76 | eqtrd 2147 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) = 〈((1st ‘𝑢) + 1), ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))〉) |
78 | 77, 67 | eqeltrd 2191 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
79 | 78 | ralrimiva 2479 |
. . . . . 6
⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
80 | | uzid 9242 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
81 | 1, 80 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑀)) |
82 | 81, 2 | opelxpd 4532 |
. . . . . 6
⊢ (𝜑 → 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶)) |
83 | 79, 82 | jca 302 |
. . . . 5
⊢ (𝜑 → (∀𝑢 ∈
((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶))) |
84 | | frecfcl 6256 |
. . . . 5
⊢
((∀𝑢 ∈
((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶)) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉):ω⟶((ℤ≥‘𝑀) × 𝐶)) |
85 | | ffn 5230 |
. . . . 5
⊢
(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉):ω⟶((ℤ≥‘𝑀) × 𝐶) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦
∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) Fn ω) |
86 | 83, 84, 85 | 3syl 17 |
. . . 4
⊢ (𝜑 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) Fn ω) |
87 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = ∅ → (𝑅‘𝑐) = (𝑅‘∅)) |
88 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = ∅ → (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅)) |
89 | 87, 88 | eqeq12d 2129 |
. . . . . . 7
⊢ (𝑐 = ∅ → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅))) |
90 | 89 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = ∅ → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅)))) |
91 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = 𝑘 → (𝑅‘𝑐) = (𝑅‘𝑘)) |
92 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) |
93 | 91, 92 | eqeq12d 2129 |
. . . . . . 7
⊢ (𝑐 = 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
94 | 93 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)))) |
95 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = suc 𝑘 → (𝑅‘𝑐) = (𝑅‘suc 𝑘)) |
96 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = suc 𝑘 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)) |
97 | 95, 96 | eqeq12d 2129 |
. . . . . . 7
⊢ (𝑐 = suc 𝑘 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘))) |
98 | 97 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = suc 𝑘 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)))) |
99 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = 𝑛 → (𝑅‘𝑐) = (𝑅‘𝑛)) |
100 | | fveq2 5375 |
. . . . . . . 8
⊢ (𝑐 = 𝑛 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛)) |
101 | 99, 100 | eqeq12d 2129 |
. . . . . . 7
⊢ (𝑐 = 𝑛 → ((𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐) ↔ (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛))) |
102 | 101 | imbi2d 229 |
. . . . . 6
⊢ (𝑐 = 𝑛 → ((𝜑 → (𝑅‘𝑐) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑐)) ↔ (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛)))) |
103 | 40 | fveq1i 5376 |
. . . . . . . 8
⊢ (𝑅‘∅) = (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) |
104 | | frec0g 6248 |
. . . . . . . . 9
⊢
(〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
105 | 82, 104 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
106 | 103, 105 | syl5eq 2159 |
. . . . . . 7
⊢ (𝜑 → (𝑅‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
107 | | frec0g 6248 |
. . . . . . . 8
⊢
(〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
108 | 82, 107 | syl 14 |
. . . . . . 7
⊢ (𝜑 → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅) = 〈𝑀, (𝐹‘𝑀)〉) |
109 | 106, 108 | eqtr4d 2150 |
. . . . . 6
⊢ (𝜑 → (𝑅‘∅) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘∅)) |
110 | 41 | ad2antlr 478 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 𝑅:ω⟶((ℤ≥‘𝑀) × 𝐶)) |
111 | | simpll 501 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 𝑘 ∈ ω) |
112 | 110, 111 | ffvelrnd 5510 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
113 | | xp1st 6017 |
. . . . . . . . . . 11
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀)) |
114 | 112, 113 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀)) |
115 | | xp2nd 6018 |
. . . . . . . . . . . 12
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶) → (2nd ‘(𝑅‘𝑘)) ∈ 𝐶) |
116 | 112, 115 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ 𝐶) |
117 | 116 | elexd 2670 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (2nd ‘(𝑅‘𝑘)) ∈ V) |
118 | | peano2uz 9280 |
. . . . . . . . . . . 12
⊢
((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) → ((1st
‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘𝑀)) |
119 | 114, 118 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘𝑀)) |
120 | 13 | ad2antlr 478 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶) |
121 | | fveq2 5375 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = ((1st
‘(𝑅‘𝑘)) + 1) → (𝐹‘𝑎) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) |
122 | 121 | eleq1d 2183 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = ((1st
‘(𝑅‘𝑘)) + 1) → ((𝐹‘𝑎) ∈ 𝐷 ↔ (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷)) |
123 | 28 | ad2antlr 478 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑎 ∈ (ℤ≥‘(𝑀 + 1))(𝐹‘𝑎) ∈ 𝐷) |
124 | | eluzp1p1 9253 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) → ((1st
‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
125 | 114, 124 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘)) + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
126 | 122, 123,
125 | rspcdva 2765 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷) |
127 | | oveq12 5737 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = (2nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) → (𝑥 + 𝑦) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
128 | 127 | eleq1d 2183 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = (2nd ‘(𝑅‘𝑘)) ∧ 𝑦 = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) → ((𝑥 + 𝑦) ∈ 𝐶 ↔ ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶)) |
129 | 128 | rspc2gv 2771 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘(𝑅‘𝑘)) ∈ 𝐶 ∧ (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)) ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶)) |
130 | 116, 126,
129 | syl2anc 406 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 (𝑥 + 𝑦) ∈ 𝐶 → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶)) |
131 | 120, 130 | mpd 13 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶) |
132 | 119, 131 | opelxpd 4532 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((2nd
‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) |
133 | | oveq1 5735 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥 + 1) = ((1st ‘(𝑅‘𝑘)) + 1)) |
134 | | fvoveq1 5751 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑥 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) |
135 | 134 | oveq2d 5744 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
136 | 133, 135 | opeq12d 3679 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
137 | | oveq1 5735 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
138 | 137 | opeq2d 3678 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), (𝑦 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((2nd
‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
139 | 136, 138,
74 | ovmpog 5859 |
. . . . . . . . . 10
⊢
(((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘(𝑅‘𝑘)) ∈ V ∧
〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
140 | 114, 117,
132, 139 | syl3anc 1199 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
141 | 79 | ad2antlr 478 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
142 | 82 | ad2antlr 478 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶)) |
143 | | frecsuc 6258 |
. . . . . . . . . . 11
⊢
((∀𝑢 ∈
((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
144 | 141, 142,
111, 143 | syl3anc 1199 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
145 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) |
146 | 145 | fveq2d 5379 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
147 | | 1st2nd2 6027 |
. . . . . . . . . . . . 13
⊢ ((𝑅‘𝑘) ∈ ((ℤ≥‘𝑀) × 𝐶) → (𝑅‘𝑘) = 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉) |
148 | 112, 147 | syl 14 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘𝑘) = 〈(1st ‘(𝑅‘𝑘)), (2nd ‘(𝑅‘𝑘))〉) |
149 | 148 | fveq2d 5379 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
150 | | df-ov 5731 |
. . . . . . . . . . 11
⊢
((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉) |
151 | 149, 150 | syl6eqr 2165 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)‘(𝑅‘𝑘)) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘)))) |
152 | 144, 146,
151 | 3eqtr2d 2153 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)(2nd ‘(𝑅‘𝑘)))) |
153 | 44 | fveq2d 5379 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉)) |
154 | | df-ov 5731 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘𝑢), (2nd
‘𝑢)〉) |
155 | 153, 154 | syl6eqr 2165 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) = ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢))) |
156 | | fvoveq1 5751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = (1st ‘𝑢) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘𝑢) + 1))) |
157 | 156 | oveq2d 5744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (1st ‘𝑢) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘𝑢) + 1)))) |
158 | | oveq1 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 = (2nd ‘𝑢) → (𝑤 + (𝐹‘((1st ‘𝑢) + 1))) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
159 | | eqid 2115 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) |
160 | 157, 158,
159 | ovmpog 5859 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘𝑢) ∈ 𝐶 ∧ ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) + 1))) ∈
𝐶) → ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
161 | 49, 51, 66, 160 | syl3anc 1199 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) = ((2nd
‘𝑢) + (𝐹‘((1st
‘𝑢) +
1)))) |
162 | 161, 66 | eqeltrd 2191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢)) ∈ 𝐶) |
163 | 54, 162 | opelxpd 4532 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) |
164 | | oveq1 5735 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = (1st ‘𝑢) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)) |
165 | 68, 164 | opeq12d 3679 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (1st ‘𝑢) → 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) |
166 | | oveq2 5736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (2nd ‘𝑢) → ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))) |
167 | 166 | opeq2d 3678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (2nd ‘𝑢) → 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
168 | | eqid 2115 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) |
169 | 165, 167,
168 | ovmpog 5859 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((1st ‘𝑢) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘𝑢) ∈ V ∧
〈((1st ‘𝑢) + 1), ((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
170 | 49, 52, 163, 169 | syl3anc 1199 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘𝑢)(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘𝑢)) = 〈((1st
‘𝑢) + 1),
((1st ‘𝑢)(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
171 | 155, 170 | eqtrd 2147 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) = 〈((1st ‘𝑢) + 1), ((1st
‘𝑢)(𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘𝑢))〉) |
172 | 171, 163 | eqeltrd 2191 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
173 | 172 | ralrimiva 2479 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
174 | 173 | ad2antlr 478 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ∀𝑢 ∈ ((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶)) |
175 | | frecsuc 6258 |
. . . . . . . . . . . . . 14
⊢
((∀𝑢 ∈
((ℤ≥‘𝑀) × 𝐶)((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘𝑢) ∈ ((ℤ≥‘𝑀) × 𝐶) ∧ 〈𝑀, (𝐹‘𝑀)〉 ∈
((ℤ≥‘𝑀) × 𝐶) ∧ 𝑘 ∈ ω) → (frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
176 | 174, 142,
111, 175 | syl3anc 1199 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘))) |
177 | 40 | fveq1i 5376 |
. . . . . . . . . . . . 13
⊢ (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘) |
178 | 40 | fveq1i 5376 |
. . . . . . . . . . . . . 14
⊢ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘) |
179 | 178 | fveq2i 5378 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) |
180 | 176, 177,
179 | 3eqtr4g 2172 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(𝑅‘𝑘))) |
181 | 148 | fveq2d 5379 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘(𝑅‘𝑘)) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
182 | 180, 181 | eqtrd 2147 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉)) |
183 | | df-ov 5731 |
. . . . . . . . . . 11
⊢
((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘))) = ((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)‘〈(1st
‘(𝑅‘𝑘)), (2nd
‘(𝑅‘𝑘))〉) |
184 | 182, 183 | syl6eqr 2165 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘)))) |
185 | | fvoveq1 5751 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝐹‘(𝑧 + 1)) = (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) |
186 | 185 | oveq2d 5744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (1st ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
187 | | oveq1 5735 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (2nd ‘(𝑅‘𝑘)) → (𝑤 + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
188 | 186, 187,
159 | ovmpog 5859 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘(𝑅‘𝑘)) ∈ 𝐶 ∧ ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1))) ∈ 𝐶) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
189 | 114, 116,
131, 188 | syl3anc 1199 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) = ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))) |
190 | 189, 131 | eqeltrd 2191 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘))) ∈ 𝐶) |
191 | 119, 190 | opelxpd 4532 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) |
192 | | oveq1 5735 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)) |
193 | 133, 192 | opeq12d 3679 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘(𝑅‘𝑘)) → 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) |
194 | | oveq2 5736 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))) |
195 | 194 | opeq2d 3678 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘(𝑅‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
196 | 193, 195,
168 | ovmpog 5859 |
. . . . . . . . . . 11
⊢
(((1st ‘(𝑅‘𝑘)) ∈ (ℤ≥‘𝑀) ∧ (2nd
‘(𝑅‘𝑘)) ∈ V ∧
〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 ∈
((ℤ≥‘𝑀) × 𝐶)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
197 | 114, 117,
191, 196 | syl3anc 1199 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → ((1st ‘(𝑅‘𝑘))(𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉)(2nd ‘(𝑅‘𝑘))) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((1st ‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉) |
198 | 189 | opeq2d 3678 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → 〈((1st
‘(𝑅‘𝑘)) + 1), ((1st
‘(𝑅‘𝑘))(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝐶 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))(2nd ‘(𝑅‘𝑘)))〉 = 〈((1st
‘(𝑅‘𝑘)) + 1), ((2nd
‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
199 | 184, 197,
198 | 3eqtrd 2151 |
. . . . . . . . 9
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = 〈((1st ‘(𝑅‘𝑘)) + 1), ((2nd ‘(𝑅‘𝑘)) + (𝐹‘((1st ‘(𝑅‘𝑘)) + 1)))〉) |
200 | 140, 152,
199 | 3eqtr4rd 2158 |
. . . . . . . 8
⊢ (((𝑘 ∈ ω ∧ 𝜑) ∧ (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)) |
201 | 200 | exp31 359 |
. . . . . . 7
⊢ (𝑘 ∈ ω → (𝜑 → ((𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘) → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)))) |
202 | 201 | a2d 26 |
. . . . . 6
⊢ (𝑘 ∈ ω → ((𝜑 → (𝑅‘𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑘)) → (𝜑 → (𝑅‘suc 𝑘) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘suc 𝑘)))) |
203 | 90, 94, 98, 102, 109, 202 | finds 4474 |
. . . . 5
⊢ (𝑛 ∈ ω → (𝜑 → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛))) |
204 | 203 | impcom 124 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ω) → (𝑅‘𝑛) = (frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)‘𝑛)) |
205 | 42, 86, 204 | eqfnfvd 5475 |
. . 3
⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
206 | 205 | rneqd 4728 |
. 2
⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
207 | | df-seqfrec 10112 |
. 2
⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) |
208 | 206, 207 | syl6reqr 2166 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) = ran 𝑅) |