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