Step |
Hyp |
Ref |
Expression |
1 |
|
suceq |
⊢ ( 𝑎 = 𝑐 → suc 𝑎 = suc 𝑐 ) |
2 |
|
oveq1 |
⊢ ( 𝑎 = 𝑐 → ( 𝑎 𝐹 𝑏 ) = ( 𝑐 𝐹 𝑏 ) ) |
3 |
1 2
|
opeq12d |
⊢ ( 𝑎 = 𝑐 → 〈 suc 𝑎 , ( 𝑎 𝐹 𝑏 ) 〉 = 〈 suc 𝑐 , ( 𝑐 𝐹 𝑏 ) 〉 ) |
4 |
|
oveq2 |
⊢ ( 𝑏 = 𝑑 → ( 𝑐 𝐹 𝑏 ) = ( 𝑐 𝐹 𝑑 ) ) |
5 |
4
|
opeq2d |
⊢ ( 𝑏 = 𝑑 → 〈 suc 𝑐 , ( 𝑐 𝐹 𝑏 ) 〉 = 〈 suc 𝑐 , ( 𝑐 𝐹 𝑑 ) 〉 ) |
6 |
3 5
|
cbvmpov |
⊢ ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ 〈 suc 𝑎 , ( 𝑎 𝐹 𝑏 ) 〉 ) = ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ 〈 suc 𝑐 , ( 𝑐 𝐹 𝑑 ) 〉 ) |
7 |
|
rdgeq1 |
⊢ ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ 〈 suc 𝑎 , ( 𝑎 𝐹 𝑏 ) 〉 ) = ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ 〈 suc 𝑐 , ( 𝑐 𝐹 𝑑 ) 〉 ) → rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ 〈 suc 𝑎 , ( 𝑎 𝐹 𝑏 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) = rec ( ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ 〈 suc 𝑐 , ( 𝑐 𝐹 𝑑 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) ) |
8 |
6 7
|
ax-mp |
⊢ rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ 〈 suc 𝑎 , ( 𝑎 𝐹 𝑏 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) = rec ( ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ 〈 suc 𝑐 , ( 𝑐 𝐹 𝑑 ) 〉 ) , 〈 ∅ , ( I ‘ 𝐼 ) 〉 ) |