Step | Hyp | Ref
| Expression |
1 | | simp1 992 |
. . . . . . . 8
⊢ ((𝐹 = 𝐺 ∧ 𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ V) → 𝐹 = 𝐺) |
2 | 1 | fveq1d 5498 |
. . . . . . 7
⊢ ((𝐹 = 𝐺 ∧ 𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ V) → (𝐹‘(𝑥 + 1)) = (𝐺‘(𝑥 + 1))) |
3 | 2 | oveq2d 5869 |
. . . . . 6
⊢ ((𝐹 = 𝐺 ∧ 𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ V) → (𝑦 + (𝐹‘(𝑥 + 1))) = (𝑦 + (𝐺‘(𝑥 + 1)))) |
4 | 3 | opeq2d 3772 |
. . . . 5
⊢ ((𝐹 = 𝐺 ∧ 𝑥 ∈ (ℤ≥‘𝑀) ∧ 𝑦 ∈ V) → 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉 = 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉) |
5 | 4 | mpoeq3dva 5917 |
. . . 4
⊢ (𝐹 = 𝐺 → (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉)) |
6 | | fveq1 5495 |
. . . . 5
⊢ (𝐹 = 𝐺 → (𝐹‘𝑀) = (𝐺‘𝑀)) |
7 | 6 | opeq2d 3772 |
. . . 4
⊢ (𝐹 = 𝐺 → 〈𝑀, (𝐹‘𝑀)〉 = 〈𝑀, (𝐺‘𝑀)〉) |
8 | | freceq1 6371 |
. . . . 5
⊢ ((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉) → frec((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉)) |
9 | | freceq2 6372 |
. . . . 5
⊢
(〈𝑀, (𝐹‘𝑀)〉 = 〈𝑀, (𝐺‘𝑀)〉 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐺‘𝑀)〉)) |
10 | 8, 9 | sylan9eq 2223 |
. . . 4
⊢ (((𝑥 ∈
(ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉) = (𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉) ∧ 〈𝑀, (𝐹‘𝑀)〉 = 〈𝑀, (𝐺‘𝑀)〉) → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐺‘𝑀)〉)) |
11 | 5, 7, 10 | syl2anc 409 |
. . 3
⊢ (𝐹 = 𝐺 → frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) = frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐺‘𝑀)〉)) |
12 | 11 | rneqd 4840 |
. 2
⊢ (𝐹 = 𝐺 → ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐺‘𝑀)〉)) |
13 | | df-seqfrec 10402 |
. 2
⊢ seq𝑀( + , 𝐹) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐹‘(𝑥 + 1)))〉), 〈𝑀, (𝐹‘𝑀)〉) |
14 | | df-seqfrec 10402 |
. 2
⊢ seq𝑀( + , 𝐺) = ran frec((𝑥 ∈ (ℤ≥‘𝑀), 𝑦 ∈ V ↦ 〈(𝑥 + 1), (𝑦 + (𝐺‘(𝑥 + 1)))〉), 〈𝑀, (𝐺‘𝑀)〉) |
15 | 12, 13, 14 | 3eqtr4g 2228 |
1
⊢ (𝐹 = 𝐺 → seq𝑀( + , 𝐹) = seq𝑀( + , 𝐺)) |