Theorem 0zs

Description: Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025)

	Ref	Expression
Assertion	0zs	⊢ 0s ∈ ℤs

Proof

Step	Hyp	Ref	Expression
1		1nns	⊢ 1s ∈ ℕs
2		1sno	⊢ 1s ∈ No
3		subsid	⊢ ( 1s ∈ No → ( 1s -s 1s ) = 0s )
4	2 3	ax-mp	⊢ ( 1s -s 1s ) = 0s
5	4	eqcomi	⊢ 0s = ( 1s -s 1s )
6		rspceov	⊢ ( ( 1s ∈ ℕs ∧ 1s ∈ ℕs ∧ 0s = ( 1s -s 1s ) ) → ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 0s = ( 𝑛 -s 𝑚 ) )
7	1 1 5 6	mp3an	⊢ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 0s = ( 𝑛 -s 𝑚 )
8		elzs	⊢ ( 0s ∈ ℤs ↔ ∃ 𝑛 ∈ ℕs ∃ 𝑚 ∈ ℕs 0s = ( 𝑛 -s 𝑚 ) )
9	7 8	mpbir	⊢ 0s ∈ ℤs