Metamath Proof Explorer

Theorem seqseq123d

Description: Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses seqseq123d.1 ⊢ ( 𝜑 → 𝑀 = 𝑁 )
seqseq123d.2 ⊢ ( 𝜑 → + = 𝑄 )
seqseq123d.3 ⊢ ( 𝜑 → 𝐹 = 𝐺 )
Assertion seqseq123d ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = seqs 𝑁 ( 𝑄 , 𝐺 ) )

Proof

Step Hyp Ref Expression
1 seqseq123d.1 ⊢ ( 𝜑 → 𝑀 = 𝑁 )
2 seqseq123d.2 ⊢ ( 𝜑 → + = 𝑄 )
3 seqseq123d.3 ⊢ ( 𝜑 → 𝐹 = 𝐺 )
4 2 oveqd ⊢ ( 𝜑 → ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) = ( 𝑦 𝑄 ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) )
5 3 fveq1d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑥 +s 1s ) ) = ( 𝐺 ‘ ( 𝑥 +s 1s ) ) )
6 5 oveq2d ⊢ ( 𝜑 → ( 𝑦 𝑄 ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) = ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) )
7 4 6 eqtrd ⊢ ( 𝜑 → ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) = ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) )
8 7 opeq2d ⊢ ( 𝜑 → ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ = ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ )
9 8 mpoeq3dv ⊢ ( 𝜑 → ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) )
10 3 1 fveq12d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) = ( 𝐺 ‘ 𝑁 ) )
11 1 10 opeq12d ⊢ ( 𝜑 → ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑁 , ( 𝐺 ‘ 𝑁 ) ⟩ )
12 rdgeq12 ⊢ ( ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) ∧ ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ = ⟨ 𝑁 , ( 𝐺 ‘ 𝑁 ) ⟩ ) → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐺 ‘ 𝑁 ) ⟩ ) )
13 9 11 12 syl2anc ⊢ ( 𝜑 → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐺 ‘ 𝑁 ) ⟩ ) )
14 13 imaeq1d ⊢ ( 𝜑 → ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐺 ‘ 𝑁 ) ⟩ ) “ ω ) )
15 df-seqs ⊢ seqs 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
16 df-seqs ⊢ seqs 𝑁 ( 𝑄 , 𝐺 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 𝑄 ( 𝐺 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑁 , ( 𝐺 ‘ 𝑁 ) ⟩ ) “ ω )
17 14 15 16 3eqtr4g ⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = seqs 𝑁 ( 𝑄 , 𝐺 ) )