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 
|- ( ph -> R = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
Assertion seqsval 
|- ( ph -> seq_s M ( .+ , F ) = ran R )

Proof

Step Hyp Ref Expression
1 seqsval.1 
 |-  ( ph -> R = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
2 df-seqs 
 |-  seq_s M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
3 eqid 
 |-  _V = _V
4 fvoveq1 
 |-  ( z = x -> ( F ` ( z +s 1s ) ) = ( F ` ( x +s 1s ) ) )
5 4 oveq2d 
 |-  ( z = x -> ( w .+ ( F ` ( z +s 1s ) ) ) = ( w .+ ( F ` ( x +s 1s ) ) ) )
6 oveq1 
 |-  ( w = y -> ( w .+ ( F ` ( x +s 1s ) ) ) = ( y .+ ( F ` ( x +s 1s ) ) ) )
7 eqid 
 |-  ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) = ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) )
8 ovex 
 |-  ( y .+ ( F ` ( x +s 1s ) ) ) e. _V
9 5 6 7 8 ovmpo 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) = ( y .+ ( F ` ( x +s 1s ) ) ) )
10 9 el2v 
 |-  ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) = ( y .+ ( F ` ( x +s 1s ) ) )
11 10 opeq2i 
 |-  <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. = <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >.
12 3 3 11 mpoeq123i 
 |-  ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) = ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. )
13 rdgeq1 
 |-  ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) = ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) -> rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) )
14 12 13 ax-mp 
 |-  rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) = rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. )
15 14 imaeq1i 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) " _om ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
16 df-ima 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) " _om ) = ran ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om )
17 2 15 16 3eqtr2i 
 |-  seq_s M ( .+ , F ) = ran ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om )
18 1 rneqd 
 |-  ( ph -> ran R = ran ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
19 17 18 eqtr4id 
 |-  ( ph -> seq_s M ( .+ , F ) = ran R )