This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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