Theorem nfseq 10380

Description: Hypothesis builder for the sequence builder operation. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Mario Carneiro, 15-Oct-2016.)

Hypotheses

Ref	Expression
nfseq.1	|- F/_ x M
nfseq.2	|- F/_ x .+
nfseq.3	|- F/_ x F

Assertion

Ref	Expression
nfseq	|- F/_ x seq M ( .+ , F )

Proof of Theorem nfseq

Dummy variables w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-seqfrec 10371	. 2 |- seq M ( .+ , F ) = ran frec ( ( z e. ( ZZ>= ` M ) , w e. _V |-> <. ( z + 1 ) , ( w .+ ( F ` ( z + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
2		nfcv 2306	. . . . . 6 |- F/_ x ZZ>=
3		nfseq.1	. . . . . 6 |- F/_ x M
4	2, 3	nffv 5490	. . . . 5 |- F/_ x ( ZZ>= ` M )
5		nfcv 2306	. . . . 5 |- F/_ x _V
6		nfcv 2306	. . . . . 6 |- F/_ x ( z + 1 )
7		nfcv 2306	. . . . . . 7 |- F/_ x w
8		nfseq.2	. . . . . . 7 |- F/_ x .+
9		nfseq.3	. . . . . . . 8 |- F/_ x F
10	9, 6	nffv 5490	. . . . . . 7 |- F/_ x ( F ` ( z + 1 ) )
11	7, 8, 10	nfov 5863	. . . . . 6 |- F/_ x ( w .+ ( F ` ( z + 1 ) ) )
12	6, 11	nfop 3768	. . . . 5 |- F/_ x <. ( z + 1 ) , ( w .+ ( F ` ( z + 1 ) ) ) >.
13	4, 5, 12	nfmpo 5902	. . . 4 |- F/_ x ( z e. ( ZZ>= ` M ) , w e. _V |-> <. ( z + 1 ) , ( w .+ ( F ` ( z + 1 ) ) ) >. )
14	9, 3	nffv 5490	. . . . 5 |- F/_ x ( F ` M )
15	3, 14	nfop 3768	. . . 4 |- F/_ x <. M , ( F ` M ) >.
16	13, 15	nffrec 6355	. . 3 |- F/_ xfrec ( ( z e. ( ZZ>= ` M ) , w e. _V |-> <. ( z + 1 ) , ( w .+ ( F ` ( z + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
17	16	nfrn 4843	. 2 |- F/_ x ran frec ( ( z e. ( ZZ>= ` M ) , w e. _V |-> <. ( z + 1 ) , ( w .+ ( F ` ( z + 1 ) ) ) >. ) , <. M , ( F ` M ) >. )
18	1, 17	nfcxfr 2303	1 |- F/_ x seq M ( .+ , F )

Syntax hints:   F/_wnfc 2293   _Vcvv 2721   <.cop 3573   ran crn 4599   ` cfv 5182  (class class class)co 5836   e. cmpo 5838  freccfrec 6349   1c1 7745   + caddc 7747   ZZ>=cuz 9457   seqcseq 10370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-rab 2451  df-v 2723  df-un 3115  df-in 3117  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-mpt 4039  df-xp 4604  df-cnv 4606  df-dm 4608  df-rn 4609  df-res 4610  df-iota 5147  df-fv 5190  df-ov 5839  df-oprab 5840  df-mpo 5841  df-recs 6264  df-frec 6350  df-seqfrec 10371

This theorem is referenced by:  seq3f1olemstep  10426  seq3f1olemp  10427  nfsum1  11283  nfsum  11284  nfcprod1  11481  nfcprod  11482