Metamath Proof Explorer


Theorem 0slt1s

Description: Surreal zero is less than surreal one. Theorem from Conway p. 7. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion 0slt1s 0 s < s 1 s

Proof

Step Hyp Ref Expression
1 0sno 0 s No
2 slerflex 0 s No 0 s s 0 s
3 1 2 ax-mp 0 s s 0 s
4 1 elexi 0 s V
5 breq2 x = 0 s 0 s s x 0 s s 0 s
6 4 5 rexsn x 0 s 0 s s x 0 s s 0 s
7 3 6 mpbir x 0 s 0 s s x
8 7 orci x 0 s 0 s s x y y s 1 s
9 0elpw 𝒫 No
10 nulssgt 𝒫 No s
11 9 10 ax-mp s
12 snssi 0 s No 0 s No
13 1 12 ax-mp 0 s No
14 snex 0 s V
15 14 elpw 0 s 𝒫 No 0 s No
16 13 15 mpbir 0 s 𝒫 No
17 nulssgt 0 s 𝒫 No 0 s s
18 16 17 ax-mp 0 s s
19 df-0s 0 s = | s
20 df-1s 1 s = 0 s | s
21 sltrec s 0 s s 0 s = | s 1 s = 0 s | s 0 s < s 1 s x 0 s 0 s s x y y s 1 s
22 11 18 19 20 21 mp4an 0 s < s 1 s x 0 s 0 s s x y y s 1 s
23 8 22 mpbir 0 s < s 1 s