Metamath Proof Explorer


Theorem seqomlem0

Description: Lemma for seqom . Change bound variables. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion seqomlem0 rec ( ( 𝑎 ∈ ω , 𝑏 ∈ V ↦ ⟨ suc 𝑎 , ( 𝑎 𝐹 𝑏 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ ) = rec ( ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ ⟨ suc 𝑐 , ( 𝑐 𝐹 𝑑 ) ⟩ ) , ⟨ ∅ , ( I ‘ 𝐼 ) ⟩ )

Proof

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 ‘ 𝐼 ) ⟩ )