Definition df-negs

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

	Ref	Expression
Assertion	df-negs	|- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnegs	|- -us
1		vx	|- x
2		cvv	|- _V
3		vn	|- n
4	3	cv	|- n
5		cright	|- _R
6	1	cv	|- x
7	6 5	cfv	|- ( _R ` x )
8	4 7	cima	|- ( n " ( _R ` x ) )
9		cscut	|- |s
10		cleft	|- _L
11	6 10	cfv	|- ( _L ` x )
12	4 11	cima	|- ( n " ( _L ` x ) )
13	8 12 9	co	|- ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) )
14	1 3 2 2 13	cmpo	|- ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) )
15	14	cnorec	|- norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) )
16	0 15	wceq	|- -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _R ` x ) ) |s ( n " ( _L ` x ) ) ) ) )