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

Metamath Proof Explorer

Theorem seqeq2

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

Ref Expression
Assertion seqeq2 ( + = 𝑄 → seq 𝑀 ( + , 𝐹 ) = seq 𝑀 ( 𝑄 , 𝐹 ) )

Proof

Step Hyp Ref Expression
1 oveq ⊢ ( + = 𝑄 → ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) = ( 𝑦 𝑄 ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) )
2 1 opeq2d ⊢ ( + = 𝑄 → ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ = ⟨ ( 𝑥 + 1 ) , ( 𝑦 𝑄 ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ )
3 2 mpoeq3dv ⊢ ( + = 𝑄 → ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 𝑄 ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) )
4 rdgeq1 ⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑦 𝑄 ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) ⟩ ) → 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 𝑀 ( 𝑄 , 𝐹 ) )