Theorem 1sno

Description: Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	1sno	Could not format assertion : No typesetting found for |- 1s e. No with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-1s	Could not format 1s = ( { 0s } |s (/) ) : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |-
2		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
3		snelpwi	Could not format ( 0s e. No -> { 0s } e. ~P No ) : No typesetting found for |- ( 0s e. No -> { 0s } e. ~P No ) with typecode |-
4	2 3	ax-mp	Could not format { 0s } e. ~P No : No typesetting found for |- { 0s } e. ~P No with typecode |-
5		nulssgt	Could not format ( { 0s } e. ~P No -> { 0s } < { 0s } <
6	4 5	ax-mp	Could not format { 0s } <
7		scutcl	Could not format ( { 0s } < ( { 0s } |s (/) ) e. No ) : No typesetting found for |- ( { 0s } < ( { 0s } |s (/) ) e. No ) with typecode |-
8	6 7	ax-mp	Could not format ( { 0s } |s (/) ) e. No : No typesetting found for |- ( { 0s } |s (/) ) e. No with typecode |-
9	1 8	eqeltri	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-