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 𝑥 𝑀
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 𝑀 ( + , 𝐹 )