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 " ( _Right ` x ) ) |s ( n " ( _Left ` 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	Could not format _Right : No typesetting found for class _Right with typecode class
6	1	cv	$$setvarx$$
7	6 5	cfv	Could not format ( _Right ` x ) : No typesetting found for class ( _Right ` x ) with typecode class
8	4 7	cima	Could not format ( n " ( _Right ` x ) ) : No typesetting found for class ( n " ( _Right ` x ) ) with typecode class
9		cscut	$$class{|}_s$$
10		cleft	Could not format _Left : No typesetting found for class _Left with typecode class
11	6 10	cfv	Could not format ( _Left ` x ) : No typesetting found for class ( _Left ` x ) with typecode class
12	4 11	cima	Could not format ( n " ( _Left ` x ) ) : No typesetting found for class ( n " ( _Left ` x ) ) with typecode class
13	8 12 9	co	Could not format ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) : No typesetting found for class ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) with typecode class
14	1 3 2 2 13	cmpo	Could not format ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) : No typesetting found for class ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) with typecode class
15	14	cnorec	Could not format norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) : No typesetting found for class norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) with typecode class
16	0 15	wceq	Could not format -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) : No typesetting found for wff -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) ) with typecode wff