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	Could not format assertion : No typesetting found for |- 0s

Proof

Step	Hyp	Ref	Expression
1		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
2		slerflex	Could not format ( 0s e. No -> 0s <_s 0s ) : No typesetting found for |- ( 0s e. No -> 0s <_s 0s ) with typecode |-
3	1 2	ax-mp	Could not format 0s <_s 0s : No typesetting found for |- 0s <_s 0s with typecode |-
4	1	elexi	Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
5		breq2	Could not format ( x = 0s -> ( 0s <_s x <-> 0s <_s 0s ) ) : No typesetting found for |- ( x = 0s -> ( 0s <_s x <-> 0s <_s 0s ) ) with typecode |-
6	4 5	rexsn	Could not format ( E. x e. { 0s } 0s <_s x <-> 0s <_s 0s ) : No typesetting found for |- ( E. x e. { 0s } 0s <_s x <-> 0s <_s 0s ) with typecode |-
7	3 6	mpbir	Could not format E. x e. { 0s } 0s <_s x : No typesetting found for |- E. x e. { 0s } 0s <_s x with typecode |-
8	7	orci	Could not format ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) : No typesetting found for |- ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) with typecode |-
9		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
10		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
11	9 10	ax-mp	$$⊢\varnothing {\ll }_s\varnothing$$
12		snssi	Could not format ( 0s e. No -> { 0s } C_ No ) : No typesetting found for |- ( 0s e. No -> { 0s } C_ No ) with typecode |-
13	1 12	ax-mp	Could not format { 0s } C_ No : No typesetting found for |- { 0s } C_ No with typecode |-
14		snex	Could not format { 0s } e. _V : No typesetting found for |- { 0s } e. _V with typecode |-
15	14	elpw	Could not format ( { 0s } e. ~P No <-> { 0s } C_ No ) : No typesetting found for |- ( { 0s } e. ~P No <-> { 0s } C_ No ) with typecode |-
16	13 15	mpbir	Could not format { 0s } e. ~P No : No typesetting found for |- { 0s } e. ~P No with typecode |-
17		nulssgt	Could not format ( { 0s } e. ~P No -> { 0s } < { 0s } <
18	16 17	ax-mp	Could not format { 0s } <
19		df-0s	Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |-
20		df-1s	Could not format 1s = ( { 0s } |s (/) ) : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |-
21		sltrec	Could not format ( ( ( (/) < ( 0s ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) ) ) : No typesetting found for |- ( ( ( (/) < ( 0s ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) ) ) with typecode |-
22	11 18 19 20 21	mp4an	Could not format ( 0s ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) ) : No typesetting found for |- ( 0s ( E. x e. { 0s } 0s <_s x \/ E. y e. (/) y <_s 1s ) ) with typecode |-
23	8 22	mpbir	Could not format 0s