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	⊢ Ⅎ 𝑥 𝑀
	nfseq.2	⊢ Ⅎ 𝑥 +
	nfseq.3	⊢ Ⅎ 𝑥 𝐹
Assertion	nfseq	⊢ Ⅎ 𝑥 seq 𝑀 ( + , 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		nfseq.1	⊢ Ⅎ 𝑥 𝑀
2		nfseq.2	⊢ Ⅎ 𝑥 +
3		nfseq.3	⊢ Ⅎ 𝑥 𝐹
4		df-seq	⊢ seq 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
5		nfcv	⊢ Ⅎ 𝑥 V
6		nfcv	⊢ Ⅎ 𝑥 ( 𝑧 + 1 )
7		nfcv	⊢ Ⅎ 𝑥 𝑤
8	3 6	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ ( 𝑧 + 1 ) )
9	7 2 8	nfov	⊢ Ⅎ 𝑥 ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) )
10	6 9	nfop	⊢ Ⅎ 𝑥 ⟨ ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ⟩
11	5 5 10	nfmpo	⊢ Ⅎ 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ⟩ )
12	3 1	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑀 )
13	1 12	nfop	⊢ Ⅎ 𝑥 ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩
14	11 13	nfrdg	⊢ Ⅎ 𝑥 rec ( ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ )
15		nfcv	⊢ Ⅎ 𝑥 ω
16	14 15	nfima	⊢ Ⅎ 𝑥 ( rec ( ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 + 1 ) , ( 𝑤 + ( 𝐹 ‘ ( 𝑧 + 1 ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
17	4 16	nfcxfr	⊢ Ⅎ 𝑥 seq 𝑀 ( + , 𝐹 )