Theorem 0sno

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

	Ref	Expression
Assertion	0sno	Could not format assertion : No typesetting found for |- 0s e. No with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-0s	Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |-
2		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
3		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
4	2 3	ax-mp	$$⊢\varnothing {\ll }_s\varnothing$$
5		scutcl	$$⊢\varnothing {\ll }_s\varnothing \to \varnothing {|}_s\varnothing \in \mathrm{No}$$
6	4 5	ax-mp	$$⊢\varnothing {|}_s\varnothing \in \mathrm{No}$$
7	1 6	eqeltri	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-