Metamath Proof Explorer

Theorem nfseqs

Description: Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses nfseqs.1 
|- F/_ x M
nfseqs.2 
|- F/_ x .+
nfseqs.3 
|- F/_ x F
Assertion nfseqs 
|- F/_ x seq_s M ( .+ , F )

Proof

Step Hyp Ref Expression
1 nfseqs.1 
 |-  F/_ x M
2 nfseqs.2 
 |-  F/_ x .+
3 nfseqs.3 
 |-  F/_ x F
4 df-seqs 
 |-  seq_s M ( .+ , F ) = ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( z .+ ( F ` ( y +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
5 nfcv 
 |-  F/_ x _V
6 nfcv 
 |-  F/_ x ( y +s 1s )
7 nfcv 
 |-  F/_ x z
8 3 6 nffv 
 |-  F/_ x ( F ` ( y +s 1s ) )
9 7 2 8 nfov 
 |-  F/_ x ( z .+ ( F ` ( y +s 1s ) ) )
10 6 9 nfop 
 |-  F/_ x <. ( y +s 1s ) , ( z .+ ( F ` ( y +s 1s ) ) ) >.
11 5 5 10 nfmpo 
 |-  F/_ x ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( z .+ ( F ` ( y +s 1s ) ) ) >. )
12 3 1 nffv 
 |-  F/_ x ( F ` M )
13 1 12 nfop 
 |-  F/_ x <. M , ( F ` M ) >.
14 11 13 nfrdg 
 |-  F/_ x rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( z .+ ( F ` ( y +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. )
15 nfcv 
 |-  F/_ x _om
16 14 15 nfima 
 |-  F/_ x ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( z .+ ( F ` ( y +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
17 4 16 nfcxfr 
 |-  F/_ x seq_s M ( .+ , F )