Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
⊢ ( 𝑀 = 𝑁 → ( 𝐹 ‘ 𝑀 ) = ( 𝐹 ‘ 𝑁 ) ) |
2 |
|
opeq12 |
⊢ ( ( 𝑀 = 𝑁 ∧ ( 𝐹 ‘ 𝑀 ) = ( 𝐹 ‘ 𝑁 ) ) → ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ ) |
3 |
1 2
|
mpdan |
⊢ ( 𝑀 = 𝑁 → ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ ) |
4 |
|
rdgeq2 |
⊢ ( ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ ) ) |
5 |
3 4
|
syl |
⊢ ( 𝑀 = 𝑁 → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ ) ) |
6 |
5
|
imaeq1d |
⊢ ( 𝑀 = 𝑁 → ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ ) “ ω ) ) |
7 |
|
df-seq |
⊢ seq 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) |
8 |
|
df-seq |
⊢ seq 𝑁 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐹 ‘ 𝑁 ) ⟩ ) “ ω ) |
9 |
6 7 8
|
3eqtr4g |
⊢ ( 𝑀 = 𝑁 → seq 𝑀 ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) ) |