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

Metamath Proof Explorer

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