Proof of Theorem seqval
Step | Hyp | Ref
| Expression |
1 | | df-ima 5051 |
. 2
⊢
(rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) = ran (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) |
2 | | df-seq 12664 |
. 2
⊢ seq𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) |
3 | | seqval.1 |
. . . 4
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) |
4 | | eqid 2610 |
. . . . . . 7
⊢ V =
V |
5 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
6 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
7 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → (𝑧 + 1) = (𝑥 + 1)) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → (𝐹‘(𝑧 + 1)) = (𝐹‘(𝑥 + 1))) |
9 | 8 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 + (𝐹‘(𝑧 + 1))) = (𝑤 + (𝐹‘(𝑥 + 1)))) |
10 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑦 → (𝑤 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
11 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) = (𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1)))) |
12 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑦 + (𝐹‘(𝑥 + 1))) ∈ V |
13 | 9, 10, 11, 12 | ovmpt2 6694 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1)))) |
14 | 5, 6, 13 | mp2an 704 |
. . . . . . . 8
⊢ (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦) = (𝑦 + (𝐹‘(𝑥 + 1))) |
15 | 14 | opeq2i 4344 |
. . . . . . 7
⊢
〈(𝑥 + 1),
(𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉 = 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉 |
16 | 4, 4, 15 | mpt2eq123i 6616 |
. . . . . 6
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) = (𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) |
17 | | rdgeq1 7394 |
. . . . . 6
⊢ ((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉) = (𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) → rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
18 | 16, 17 | ax-mp 5 |
. . . . 5
⊢
rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) = rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) |
19 | 18 | reseq1i 5313 |
. . . 4
⊢
(rec((𝑥 ∈ V,
𝑦 ∈ V ↦
〈(𝑥 + 1), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 + 1))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) |
20 | 3, 19 | eqtri 2632 |
. . 3
⊢ 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) |
21 | 20 | rneqi 5273 |
. 2
⊢ ran 𝑅 = ran (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω) |
22 | 1, 2, 21 | 3eqtr4i 2642 |
1
⊢ seq𝑀( + , 𝐹) = ran 𝑅 |