Metamath Proof Explorer

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 " ( _Right ` x ) ) |s ( n " ( _Left ` 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 
 |-  _Right
6 1 cv 
 |-  x
7 6 5 cfv 
 |-  ( _Right ` x )
8 4 7 cima 
 |-  ( n " ( _Right ` x ) )
9 cscut 
 |-  |s
10 cleft 
 |-  _Left
11 6 10 cfv 
 |-  ( _Left ` x )
12 4 11 cima 
 |-  ( n " ( _Left ` x ) )
13 8 12 9 co 
 |-  ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) )
14 1 3 2 2 13 cmpo 
 |-  ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) )
15 14 cnorec 
 |-  norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) )
16 0 15 wceq 
 |-  -us = norec ( ( x e. _V , n e. _V |-> ( ( n " ( _Right ` x ) ) |s ( n " ( _Left ` x ) ) ) ) )