Theorem seqeq1

Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

	Ref	Expression
Assertion	seqeq1	⊢ ( 𝑀 = 𝑁 → seq 𝑀 ( + , 𝐹 ) = seq 𝑁 ( + , 𝐹 ) )

Proof

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 𝑁 ( + , 𝐹 ) )