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