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 )