Theorem nfseqs

Description: Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	nfseqs.1	⊢ Ⅎ 𝑥 𝑀
	nfseqs.2	⊢ Ⅎ 𝑥 +
	nfseqs.3	⊢ Ⅎ 𝑥 𝐹
Assertion	nfseqs	⊢ Ⅎ 𝑥 seqs 𝑀 ( + , 𝐹 )

Proof

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