This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfseq

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

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

Proof

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