Theorem noseqno

Description: An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		noseq.1	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐴 ) “ ω ) )
2		noseq.2	⊢ ( 𝜑 → 𝐴 ∈ No )
3		noseqno.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑍 )
4	1 2	noseqssno	⊢ ( 𝜑 → 𝑍 ⊆ No )
5	4 3	sseldd	⊢ ( 𝜑 → 𝐵 ∈ No )