Metamath Proof Explorer

Theorem seqsval

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

Ref Expression
Hypothesis seqsval.1 ⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
Assertion seqsval ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = ran 𝑅 )

Proof

Step Hyp Ref Expression
1 seqsval.1 ⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
2 df-seqs ⊢ seqs 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
3 eqid ⊢ V = V
4 fvoveq1 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ ( 𝑧 +s 1s ) ) = ( 𝐹 ‘ ( 𝑥 +s 1s ) ) )
5 4 oveq2d ⊢ ( 𝑧 = 𝑥 → ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) = ( 𝑤 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) )
6 oveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) = ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) )
7 eqid ⊢ ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) = ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) )
8 ovex ⊢ ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ∈ V
9 5 6 7 8 ovmpo ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) = ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) )
10 9 el2v ⊢ ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) = ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) )
11 10 opeq2i ⊢ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ = ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩
12 3 3 11 mpoeq123i ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ )
13 rdgeq1 ⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) → rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) )
14 12 13 ax-mp ⊢ rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) = rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ )
15 14 imaeq1i ⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
16 df-ima ⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
17 2 15 16 3eqtr2i ⊢ seqs 𝑀 ( + , 𝐹 ) = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω )
18 1 rneqd ⊢ ( 𝜑 → ran 𝑅 = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
19 17 18 eqtr4id ⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = ran 𝑅 )