Theorem reno

Description: A surreal real is a surreal number. (Contributed by Scott Fenton, 19-Feb-2026)

	Ref	Expression
Assertion	reno	⊢ ( 𝐴 ∈ ℝs → 𝐴 ∈ No )

Proof

Step	Hyp	Ref	Expression
1		elreno	⊢ ( 𝐴 ∈ ℝs ↔ ( 𝐴 ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 𝐴 ∧ 𝐴 <s 𝑛 ) ∧ 𝐴 = ( { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 -s ( 1s /su 𝑛 ) ) } |s { 𝑥 ∣ ∃ 𝑛 ∈ ℕs 𝑥 = ( 𝐴 +s ( 1s /su 𝑛 ) ) } ) ) ) )
2	1	simplbi	⊢ ( 𝐴 ∈ ℝs → 𝐴 ∈ No )