Definition df-negs

Description: Define surreal negation. Definition from Conway p. 5. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	df-negs	Could not format assertion : No typesetting found for |- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnegs	Could not format -us : No typesetting found for class -us with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vn	$$setvarn$$
4	3	cv	$$setvarn$$
5		cright	$$classR$$
6	1	cv	$$setvarx$$
7	6 5	cfv	$$classR\left(x\right)$$
8	4 7	cima	$$classn\left[R\left(x\right)\right]$$
9		cscut	$$class{|}_s$$
10		cleft	$$classL$$
11	6 10	cfv	$$classL\left(x\right)$$
12	4 11	cima	$$classn\left[L\left(x\right)\right]$$
13	8 12 9	co	$$class\left(n\left[R\left(x\right)\right]{|}_{s}n\left[L\left(x\right)\right]\right)$$
14	1 3 2 2 13	cmpo	$$class\left(x\in \mathrm{V},n\in \mathrm{V}⟼n\left[R\left(x\right)\right]{|}_{s}n\left[L\left(x\right)\right]\right)$$
15	14	cnorec	Could not format norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) : No typesetting found for class norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) with typecode class
16	0 15	wceq	Could not format -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) : No typesetting found for wff -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) ) with typecode wff