Theorem 1no

Description: Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	1no	$$⊢1_s\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		df-1s	$$⊢1_s=\left\{0_s\right\}{|}_s\varnothing$$
2		0no	$$⊢0_s\in \mathrm{No}$$
3		snelpwi	$$⊢0_s\in \mathrm{No}\to \left\{0_s\right\}\in 𝒫\mathrm{No}$$
4	2 3	ax-mp	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}$$
5		nulsgts	$$⊢\left\{0_s\right\}\in 𝒫\mathrm{No}\to \left\{0_s\right\}{\ll }_s\varnothing$$
6	4 5	ax-mp	$$⊢\left\{0_s\right\}{\ll }_s\varnothing$$
7		cutscl	$$⊢\left\{0_s\right\}{\ll }_s\varnothing \to \left\{0_s\right\}{|}_s\varnothing \in \mathrm{No}$$
8	6 7	ax-mp	$$⊢\left\{0_s\right\}{|}_s\varnothing \in \mathrm{No}$$
9	1 8	eqeltri	$$⊢1_s\in \mathrm{No}$$