Theorem 0lt1s

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

	Ref	Expression
Assertion	0lt1s	⊢ 0s <s 1s

Proof

Step	Hyp	Ref	Expression
1		0no	⊢ 0s ∈ No
2		lesid	⊢ ( 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		nulsgts	⊢ ( ∅ ∈ 𝒫 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		nulsgts	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
18	16 17	ax-mp	⊢ { 0s } <<s ∅
19		df-0s	⊢ 0s = ( ∅ |s ∅ )
20		df-1s	⊢ 1s = ( { 0s } |s ∅ )
21		ltsrec	⊢ ( ( ( ∅ <<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