Theorem reno

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

	Ref	Expression
Assertion	reno	$$⊢A\in {ℝ}_s\to A\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		elreno	$$⊢A\in {ℝ}_s\leftrightarrow \left(A\in \mathrm{No}\wedge \left(\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_{s}A\wedge A{<}_{s}n\right)\wedge A=\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{-}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}{|}_s\left\{x|\exists n\in {\mathbb{N}}_{s}x=A{+}_s\left(1_s{/}_{\mathrm{su}}n\right)\right\}\right)\right)$$
2	1	simplbi	$$⊢A\in {ℝ}_s\to A\in \mathrm{No}$$