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