Theorem 1n0s

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

	Ref	Expression
Assertion	1n0s	⊢ 1s ∈ ℕ0s

Proof

Step	Hyp	Ref	Expression
1		1sno	⊢ 1s ∈ No
2		addslid	⊢ ( 1s ∈ No → ( 0s +s 1s ) = 1s )
3	1 2	ax-mp	⊢ ( 0s +s 1s ) = 1s
4		0n0s	⊢ 0s ∈ ℕ0s
5		peano2n0s	⊢ ( 0s ∈ ℕ0s → ( 0s +s 1s ) ∈ ℕ0s )
6	4 5	ax-mp	⊢ ( 0s +s 1s ) ∈ ℕ0s
7	3 6	eqeltrri	⊢ 1s ∈ ℕ0s