Theorem noseqssno

Description: A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
	noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
Assertion	noseqssno	⊢ ( 𝜑 → 𝑍 ⊆ No )

Proof

Step	Hyp	Ref	Expression
1		noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
2		noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
3		peano2no	⊢ ( 𝑦 ∈ No → ( 𝑦 +s 1s ) ∈ No )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ No ) → ( 𝑦 +s 1s ) ∈ No )
5	1 2 2 4	noseqind	⊢ ( 𝜑 → 𝑍 ⊆ No )