Metamath Proof Explorer

Theorem seqsex

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

Ref Expression
Assertion seqsex 
|- seq_s M ( .+ , F ) e. _V

Proof

Step Hyp Ref Expression
1 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 )
2 rdgfun 
 |-  Fun rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. )
3 dcomex 
 |-  _om e. _V
4 3 funimaex 
 |-  ( Fun rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) -> ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) e. _V )
5 2 4 ax-mp 
 |-  ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om ) e. _V
6 1 5 eqeltri 
 |-  seq_s M ( .+ , F ) e. _V