Theorem seqeq3

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

	Ref	Expression
Assertion	seqeq3	⊢ ( 𝐹 = 𝐺 → seq 𝑀 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 ‘ ( 𝑥 + 1 ) ) = ( 𝐺 ‘ ( 𝑥 + 1 ) ) )
2	1	oveq2d	⊢ ( 𝐹 = 𝐺 → ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) = ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) )
3	2	opeq2d	⊢ ( 𝐹 = 𝐺 → ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ = ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
4	3	mpoeq3dv	⊢ ( 𝐹 = 𝐺 → ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) )
5		fveq1	⊢ ( 𝐹 = 𝐺 → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ 𝑀 ) )
6	5	opeq2d	⊢ ( 𝐹 = 𝐺 → ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑀 , ( 𝐺 ‘ 𝑀 ) ⟩ )
7		rdgeq12	⊢ ( ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) ∧ ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑀 , ( 𝐺 ‘ 𝑀 ) ⟩ ) → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐺 ‘ 𝑀 ) ⟩ ) )
8	4 6 7	syl2anc	⊢ ( 𝐹 = 𝐺 → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐺 ‘ 𝑀 ) ⟩ ) )
9	8	imaeq1d	⊢ ( 𝐹 = 𝐺 → ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐺 ‘ 𝑀 ) ⟩ ) “ ω ) )
10		df-seq	⊢ seq 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
11		df-seq	⊢ seq 𝑀 ( + , 𝐺 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐺 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐺 ‘ 𝑀 ) ⟩ ) “ ω )
12	9 10 11	3eqtr4g	⊢ ( 𝐹 = 𝐺 → seq 𝑀 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐺 ) )