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 
|- ( ph -> M e. No )
seqsp1.2 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) )
seqsp1.3 
|- ( ph -> N e. Z )
Assertion seqsp1 
|- ( ph -> ( seq_s M ( .+ , F ) ` ( N +s 1s ) ) = ( ( seq_s M ( .+ , F ) ` N ) .+ ( F ` ( N +s 1s ) ) ) )

Proof

Step Hyp Ref Expression
1 seqsp1.1 
 |-  ( ph -> M e. No )
2 seqsp1.2 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) )
3 seqsp1.3 
 |-  ( ph -> N e. Z )
4 eqidd 
 |-  ( ph -> ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) |` _om ) = ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) |` _om ) )
5 oveq1 
 |-  ( x = y -> ( x +s 1s ) = ( y +s 1s ) )
6 5 cbvmptv 
 |-  ( x e. _V |-> ( x +s 1s ) ) = ( y e. _V |-> ( y +s 1s ) )
7 rdgeq1 
 |-  ( ( x e. _V |-> ( x +s 1s ) ) = ( y e. _V |-> ( y +s 1s ) ) -> rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) = rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) )
8 6 7 ax-mp 
 |-  rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) = rec ( ( y e. _V |-> ( y +s 1s ) ) , M )
9 8 imaeq1i 
 |-  ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) = ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) " _om )
10 2 9 eqtrdi 
 |-  ( ph -> Z = ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) " _om ) )
11 fvexd 
 |-  ( ph -> ( F ` M ) e. _V )
12 eqidd 
 |-  ( ph -> ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( y ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) z ) >. ) , <. M , ( F ` M ) >. ) |` _om ) = ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( y ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) z ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
13 12 seqsval 
 |-  ( ph -> seq_s M ( .+ , F ) = ran ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( y ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) z ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
14 1 4 10 11 12 13 noseqrdgsuc 
 |-  ( ( ph /\ N e. Z ) -> ( seq_s M ( .+ , F ) ` ( N +s 1s ) ) = ( N ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) ( seq_s M ( .+ , F ) ` N ) ) )
15 3 14 mpdan 
 |-  ( ph -> ( seq_s M ( .+ , F ) ` ( N +s 1s ) ) = ( N ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) ( seq_s M ( .+ , F ) ` N ) ) )
16 3 elexd 
 |-  ( ph -> N e. _V )
17 fvex 
 |-  ( seq_s M ( .+ , F ) ` N ) e. _V
18 fvoveq1 
 |-  ( w = N -> ( F ` ( w +s 1s ) ) = ( F ` ( N +s 1s ) ) )
19 18 oveq2d 
 |-  ( w = N -> ( t .+ ( F ` ( w +s 1s ) ) ) = ( t .+ ( F ` ( N +s 1s ) ) ) )
20 oveq1 
 |-  ( t = ( seq_s M ( .+ , F ) ` N ) -> ( t .+ ( F ` ( N +s 1s ) ) ) = ( ( seq_s M ( .+ , F ) ` N ) .+ ( F ` ( N +s 1s ) ) ) )
21 eqid 
 |-  ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) = ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) )
22 ovex 
 |-  ( ( seq_s M ( .+ , F ) ` N ) .+ ( F ` ( N +s 1s ) ) ) e. _V
23 19 20 21 22 ovmpo 
 |-  ( ( N e. _V /\ ( seq_s M ( .+ , F ) ` N ) e. _V ) -> ( N ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) ( seq_s M ( .+ , F ) ` N ) ) = ( ( seq_s M ( .+ , F ) ` N ) .+ ( F ` ( N +s 1s ) ) ) )
24 16 17 23 sylancl 
 |-  ( ph -> ( N ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) ( seq_s M ( .+ , F ) ` N ) ) = ( ( seq_s M ( .+ , F ) ` N ) .+ ( F ` ( N +s 1s ) ) ) )
25 15 24 eqtrd 
 |-  ( ph -> ( seq_s M ( .+ , F ) ` ( N +s 1s ) ) = ( ( seq_s M ( .+ , F ) ` N ) .+ ( F ` ( N +s 1s ) ) ) )