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	$$⊢\underset{\_}{Ⅎ}xM$$
	nfseq.2	$$⊢\underset{\_}{Ⅎ}x\underset{\dot{}}{+}$$
	nfseq.3	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	nfseq	$$⊢\underset{\_}{Ⅎ}xseqM\left(\underset{\dot{}}{+},F\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfseq.1	$$⊢\underset{\_}{Ⅎ}xM$$
2		nfseq.2	$$⊢\underset{\_}{Ⅎ}x\underset{\dot{}}{+}$$
3		nfseq.3	$$⊢\underset{\_}{Ⅎ}xF$$
4		df-seq	$$⊢seqM\left(\underset{\dot{}}{+},F\right)=\mathrm{rec}\left(\left(z\in \mathrm{V},w\in \mathrm{V}⟼⟨z+1,w\underset{\dot{}}{+}F\left(z+1\right)⟩\right),⟨M,F\left(M\right)⟩\right)\left[\mathrm{\omega }\right]$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(z+1\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xw$$
8	3 6	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z+1\right)$$
9	7 2 8	nfov	$$⊢\underset{\_}{Ⅎ}x\left(w\underset{\dot{}}{+}F\left(z+1\right)\right)$$
10	6 9	nfop	$$⊢\underset{\_}{Ⅎ}x⟨z+1,w\underset{\dot{}}{+}F\left(z+1\right)⟩$$
11	5 5 10	nfmpo	$$⊢\underset{\_}{Ⅎ}x\left(z\in \mathrm{V},w\in \mathrm{V}⟼⟨z+1,w\underset{\dot{}}{+}F\left(z+1\right)⟩\right)$$
12	3 1	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(M\right)$$
13	1 12	nfop	$$⊢\underset{\_}{Ⅎ}x⟨M,F\left(M\right)⟩$$
14	11 13	nfrdg	$$⊢\underset{\_}{Ⅎ}x\mathrm{rec}\left(\left(z\in \mathrm{V},w\in \mathrm{V}⟼⟨z+1,w\underset{\dot{}}{+}F\left(z+1\right)⟩\right),⟨M,F\left(M\right)⟩\right)$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{\omega }$$
16	14 15	nfima	$$⊢\underset{\_}{Ⅎ}x\mathrm{rec}\left(\left(z\in \mathrm{V},w\in \mathrm{V}⟼⟨z+1,w\underset{\dot{}}{+}F\left(z+1\right)⟩\right),⟨M,F\left(M\right)⟩\right)\left[\mathrm{\omega }\right]$$
17	4 16	nfcxfr	$$⊢\underset{\_}{Ⅎ}xseqM\left(\underset{\dot{}}{+},F\right)$$