Step | Hyp | Ref
| Expression |
1 | | iseqval.1 |
. . . 4
⊢ 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) |
2 | | simprl 497 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (ℤ≥‘𝑀)) |
3 | | simprr 498 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
4 | | iseqval.pl |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
5 | 4 | caovclg 5673 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆) |
6 | 5 | adantlr 460 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) ∧ (𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆)) → (𝑎 + 𝑏) ∈ 𝑆) |
7 | | iseqval.f |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑥) ∈ 𝑆) |
8 | 7 | ralrimiva 2434 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ (ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆) |
9 | | fveq2 5198 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
10 | 9 | eleq1d 2147 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ 𝑆 ↔ (𝐹‘𝑦) ∈ 𝑆)) |
11 | 10 | cbvralv 2577 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
(ℤ≥‘𝑀)(𝐹‘𝑥) ∈ 𝑆 ↔ ∀𝑦 ∈ (ℤ≥‘𝑀)(𝐹‘𝑦) ∈ 𝑆) |
12 | 8, 11 | sylib 120 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ (ℤ≥‘𝑀)(𝐹‘𝑦) ∈ 𝑆) |
13 | 12 | adantr 270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → ∀𝑦 ∈ (ℤ≥‘𝑀)(𝐹‘𝑦) ∈ 𝑆) |
14 | | peano2uz 8671 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (𝑥 + 1) ∈
(ℤ≥‘𝑀)) |
15 | | fveq2 5198 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 + 1) → (𝐹‘𝑦) = (𝐹‘(𝑥 + 1))) |
16 | 15 | eleq1d 2147 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 + 1) → ((𝐹‘𝑦) ∈ 𝑆 ↔ (𝐹‘(𝑥 + 1)) ∈ 𝑆)) |
17 | 16 | rspcv 2697 |
. . . . . . . . . . . . 13
⊢ ((𝑥 + 1) ∈
(ℤ≥‘𝑀) → (∀𝑦 ∈ (ℤ≥‘𝑀)(𝐹‘𝑦) ∈ 𝑆 → (𝐹‘(𝑥 + 1)) ∈ 𝑆)) |
18 | 14, 17 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
(ℤ≥‘𝑀) → (∀𝑦 ∈ (ℤ≥‘𝑀)(𝐹‘𝑦) ∈ 𝑆 → (𝐹‘(𝑥 + 1)) ∈ 𝑆)) |
19 | 18 | ad2antrl 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (∀𝑦 ∈ (ℤ≥‘𝑀)(𝐹‘𝑦) ∈ 𝑆 → (𝐹‘(𝑥 + 1)) ∈ 𝑆)) |
20 | 13, 19 | mpd 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝐹‘(𝑥 + 1)) ∈ 𝑆) |
21 | 6, 3, 20 | caovcld 5674 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝑆) |
22 | | oveq1 5539 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1)) |
23 | 22 | fveq2d 5202 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1))) |
24 | 23 | oveq2d 5548 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘(𝑥 + 1)))) |
25 | | oveq1 5539 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
26 | | eqid 2081 |
. . . . . . . . . 10
⊢ (𝑧 ∈
(ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) |
27 | 24, 25, 26 | ovmpt2g 5655 |
. . . . . . . . 9
⊢ ((𝑥 ∈
(ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆 ∧ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ 𝑆) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
28 | 2, 3, 21, 27 | syl3anc 1169 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
29 | 28 | 3impb 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆) → (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
30 | 29 | opeq2d 3577 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ 𝑆) → 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) |
31 | 30 | mpt2eq3dva 5589 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉)) |
32 | | freceq1 6002 |
. . . . 5
⊢ ((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) → frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
33 | 31, 32 | syl 14 |
. . . 4
⊢ (𝜑 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ (ℤ≥‘𝑀), 𝑤 ∈ 𝑆 ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
34 | 1, 33 | syl5eq 2125 |
. . 3
⊢ (𝜑 → 𝑅 = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
35 | 34 | rneqd 4581 |
. 2
⊢ (𝜑 → ran 𝑅 = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
36 | | df-iseq 9432 |
. 2
⊢ seq𝑀( + , 𝐹, 𝑆) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ 𝑆 ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) |
37 | 35, 36 | syl6reqr 2132 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹, 𝑆) = ran 𝑅) |