Theorem 1n0s

Description: Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Assertion	1n0s	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$

Proof

Step	Hyp	Ref	Expression
1		1no	$$⊢1_s\in \mathrm{No}$$
2		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
3	1 2	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
4		0n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}$$
5		peano2n0s	$$⊢0_s\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
6	4 5	ax-mp	$$⊢0_s{+}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$
7	3 6	eqeltrri	$$⊢1_s\in {\mathbb{N}}_{\mathrm{0s}}$$