Theorem n0ssno

Description: The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025)

	Ref	Expression
Assertion	n0ssno	Could not format assertion : No typesetting found for |- NN0_s C_ No with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-n0s	Could not format NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) : No typesetting found for |- NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) with typecode |-
2	1	a1i	Could not format ( T. -> NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) ) : No typesetting found for |- ( T. -> NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) ) with typecode |-
3		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
4	3	a1i	Could not format ( T. -> 0s e. No ) : No typesetting found for |- ( T. -> 0s e. No ) with typecode |-
5	2 4	noseqssno	Could not format ( T. -> NN0_s C_ No ) : No typesetting found for |- ( T. -> NN0_s C_ No ) with typecode |-
6	5	mptru	Could not format NN0_s C_ No : No typesetting found for |- NN0_s C_ No with typecode |-