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 0s <s 1s

Proof

Step Hyp Ref Expression
1 0sno 0s ∈ No
2 slerflex ( 0s ∈ No → 0s ≤s 0s )
3 1 2 ax-mp 0s ≤s 0s
4 1 elexi 0s ∈ V
5 breq2 ( 𝑥 = 0s → ( 0s ≤s 𝑥 ↔ 0s ≤s 0s ) )
6 4 5 rexsn ( ∃ 𝑥 ∈ { 0s } 0s ≤s 𝑥 ↔ 0s ≤s 0s )
7 3 6 mpbir 𝑥 ∈ { 0s } 0s ≤s 𝑥
8 7 orci ( ∃ 𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃ 𝑦 ∈ ∅ 𝑦 ≤s 1s )
9 0elpw ∅ ∈ 𝒫 No
10 nulssgt ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
11 9 10 ax-mp ∅ <<s ∅
12 snssi ( 0s ∈ No → { 0s } ⊆ No )
13 1 12 ax-mp { 0s } ⊆ No
14 snex { 0s } ∈ V
15 14 elpw ( { 0s } ∈ 𝒫 No ↔ { 0s } ⊆ No )
16 13 15 mpbir { 0s } ∈ 𝒫 No
17 nulssgt ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
18 16 17 ax-mp { 0s } <<s ∅
19 df-0s 0s = ( ∅ |s ∅ )
20 df-1s 1s = ( { 0s } |s ∅ )
21 sltrec ( ( ( ∅ <<s ∅ ∧ { 0s } <<s ∅ ) ∧ ( 0s = ( ∅ |s ∅ ) ∧ 1s = ( { 0s } |s ∅ ) ) ) → ( 0s <s 1s ↔ ( ∃ 𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃ 𝑦 ∈ ∅ 𝑦 ≤s 1s ) ) )
22 11 18 19 20 21 mp4an ( 0s <s 1s ↔ ( ∃ 𝑥 ∈ { 0s } 0s ≤s 𝑥 ∨ ∃ 𝑦 ∈ ∅ 𝑦 ≤s 1s ) )
23 8 22 mpbir 0s <s 1s