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

Proof

Step	Hyp	Ref	Expression
1		0sno	|- 0s e. No
2		slerflex	|- ( 0s e. No -> 0s <_s 0s )
3	1 2	ax-mp	|- 0s <_s 0s
4	1	elexi	|- 0s e. _V
5		breq2	|- ( x = 0s -> ( 0s <_s x <-> 0s <_s 0s ) )
6	4 5	rexsn	|- ( E. x e. { 0s } 0s <_s x <-> 0s <_s 0s )
7	3 6	mpbir	|- E. x e. { 0s } 0s <_s x
8	7	orci	|- ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s )
9		0elpw	|- (/) e. ~P No
10		nulssgt	|- ( (/) e. ~P No -> (/) <
11	9 10	ax-mp	|- (/) <
12		snssi	|- ( 0s e. No -> { 0s } C_ No )
13	1 12	ax-mp	|- { 0s } C_ No
14		snex	|- { 0s } e. _V
15	14	elpw	|- ( { 0s } e. ~P No <-> { 0s } C_ No )
16	13 15	mpbir	|- { 0s } e. ~P No
17		nulssgt	|- ( { 0s } e. ~P No -> { 0s } <
18	16 17	ax-mp	|- { 0s } <
19		df-0s	|- 0s = ( (/) |s (/) )
20		df-1s	|- 1s = ( { 0s } |s (/) )
21		sltrec	|- ( ( ( (/) < ( 0s ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) ) )
22	11 18 19 20 21	mp4an	|- ( 0s ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) )
23	8 22	mpbir	|- 0s