Metamath Proof Explorer


Theorem 0sno

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

Ref Expression
Assertion 0sno 0s ∈ No

Proof

Step Hyp Ref Expression
1 df-0s 0s = ( ∅ |s ∅ )
2 0elpw ∅ ∈ 𝒫 No
3 nulssgt ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
4 2 3 ax-mp ∅ <<s ∅
5 scutcl ( ∅ <<s ∅ → ( ∅ |s ∅ ) ∈ No )
6 4 5 ax-mp ( ∅ |s ∅ ) ∈ No
7 1 6 eqeltri 0s ∈ No