Description: Surreal zero is a surreal. (Contributed by Scott Fenton, 7-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 0sno | ⊢ 0s ∈ No |
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 |