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

Metamath Proof Explorer

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 𝑀 ( + , 𝐺 ) )