Metamath Proof Explorer

Theorem seqsp1

Description: The value of the surreal sequence builder at a successor. (Contributed by Scott Fenton, 19-Apr-2025)

Ref Expression
Hypotheses seqsp1.1 ⊢ ( 𝜑 → 𝑀 ∈ No )
seqsp1.2 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) )
seqsp1.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
Assertion seqsp1 ( 𝜑 → ( seqs 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 +s 1s ) ) = ( ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) )

Proof

Step Hyp Ref Expression
1 seqsp1.1 ⊢ ( 𝜑 → 𝑀 ∈ No )
2 seqsp1.2 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) )
3 seqsp1.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
4 eqidd ⊢ ( 𝜑 → ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) ↾ ω ) )
5 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 +s 1s ) = ( 𝑦 +s 1s ) )
6 5 cbvmptv ⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) = ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) )
7 rdgeq1 ⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) = ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) → rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) = rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) )
8 6 7 ax-mp ⊢ rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) = rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 )
9 8 imaeq1i ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) “ ω )
10 2 9 eqtrdi ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) “ ω ) )
11 fvexd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ V )
12 eqidd ⊢ ( 𝜑 → ( rec ( ( 𝑦 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑦 +s 1s ) , ( 𝑦 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) 𝑧 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑦 +s 1s ) , ( 𝑦 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) 𝑧 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
13 12 seqsval ⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = ran ( rec ( ( 𝑦 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑦 +s 1s ) , ( 𝑦 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) 𝑧 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
14 1 4 10 11 12 13 noseqrdgsuc ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝑍 ) → ( seqs 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 +s 1s ) ) = ( 𝑁 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
15 3 14 mpdan ⊢ ( 𝜑 → ( seqs 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 +s 1s ) ) = ( 𝑁 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
16 3 elexd ⊢ ( 𝜑 → 𝑁 ∈ V )
17 fvex ⊢ ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V
18 fvoveq1 ⊢ ( 𝑤 = 𝑁 → ( 𝐹 ‘ ( 𝑤 +s 1s ) ) = ( 𝐹 ‘ ( 𝑁 +s 1s ) ) )
19 18 oveq2d ⊢ ( 𝑤 = 𝑁 → ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) = ( 𝑡 + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) )
20 oveq1 ⊢ ( 𝑡 = ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) → ( 𝑡 + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) = ( ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) )
21 eqid ⊢ ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) = ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) )
22 ovex ⊢ ( ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) ∈ V
23 19 20 21 22 ovmpo ⊢ ( ( 𝑁 ∈ V ∧ ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ V ) → ( 𝑁 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) )
24 16 17 23 sylancl ⊢ ( 𝜑 → ( 𝑁 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) )
25 15 24 eqtrd ⊢ ( 𝜑 → ( seqs 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 +s 1s ) ) = ( ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( 𝐹 ‘ ( 𝑁 +s 1s ) ) ) )