Metamath Proof Explorer

Theorem negright

Description: The right set of the negative of a surreal is the set of negatives of its left set. (Contributed by Scott Fenton, 21-Feb-2026)

Ref Expression
Assertion negright 
|- ( A e. No -> ( _Right ` ( -us ` A ) ) = ( -us " ( _Left ` A ) ) )

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( y = ( -us ` x ) -> ( ( -us ` y ) = x <-> ( -us ` ( -us ` x ) ) = x ) )
2 rightold 
 |-  ( x e. ( _Right ` ( -us ` A ) ) -> x e. ( _Old ` ( bday ` ( -us ` A ) ) ) )
3 2 adantl 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> x e. ( _Old ` ( bday ` ( -us ` A ) ) ) )
4 bdayon 
 |-  ( bday ` ( -us ` A ) ) e. On
5 rightno 
 |-  ( x e. ( _Right ` ( -us ` A ) ) -> x e. No )
6 5 adantl 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> x e. No )
7 oldbday 
 |-  ( ( ( bday ` ( -us ` A ) ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` ( -us ` A ) ) ) <-> ( bday ` x ) e. ( bday ` ( -us ` A ) ) ) )
8 4 6 7 sylancr 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( x e. ( _Old ` ( bday ` ( -us ` A ) ) ) <-> ( bday ` x ) e. ( bday ` ( -us ` A ) ) ) )
9 3 8 mpbid 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( bday ` x ) e. ( bday ` ( -us ` A ) ) )
10 negbday 
 |-  ( x e. No -> ( bday ` ( -us ` x ) ) = ( bday ` x ) )
11 6 10 syl 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( bday ` ( -us ` x ) ) = ( bday ` x ) )
12 negbday 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
13 12 adantr 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
14 13 eqcomd 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( bday ` A ) = ( bday ` ( -us ` A ) ) )
15 9 11 14 3eltr4d 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( bday ` ( -us ` x ) ) e. ( bday ` A ) )
16 bdayon 
 |-  ( bday ` A ) e. On
17 6 negscld 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` x ) e. No )
18 oldbday 
 |-  ( ( ( bday ` A ) e. On /\ ( -us ` x ) e. No ) -> ( ( -us ` x ) e. ( _Old ` ( bday ` A ) ) <-> ( bday ` ( -us ` x ) ) e. ( bday ` A ) ) )
19 16 17 18 sylancr 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( ( -us ` x ) e. ( _Old ` ( bday ` A ) ) <-> ( bday ` ( -us ` x ) ) e. ( bday ` A ) ) )
20 15 19 mpbird 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` x ) e. ( _Old ` ( bday ` A ) ) )
21 rightgt 
 |-  ( x e. ( _Right ` ( -us ` A ) ) -> ( -us ` A )
22 21 adantl 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` A )
23 simpl 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> A e. No )
24 23 negscld 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` A ) e. No )
25 24 6 ltnegsd 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( ( -us ` A )  ( -us ` x )
26 22 25 mpbid 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` x )
27 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
28 27 adantr 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` ( -us ` A ) ) = A )
29 26 28 breqtrd 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` x )
30 elleft 
 |-  ( ( -us ` x ) e. ( _Left ` A ) <-> ( ( -us ` x ) e. ( _Old ` ( bday ` A ) ) /\ ( -us ` x )
31 20 29 30 sylanbrc 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` x ) e. ( _Left ` A ) )
32 negnegs 
 |-  ( x e. No -> ( -us ` ( -us ` x ) ) = x )
33 6 32 syl 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> ( -us ` ( -us ` x ) ) = x )
34 1 31 33 rspcedvdw 
 |-  ( ( A e. No /\ x e. ( _Right ` ( -us ` A ) ) ) -> E. y e. ( _Left ` A ) ( -us ` y ) = x )
35 34 ex 
 |-  ( A e. No -> ( x e. ( _Right ` ( -us ` A ) ) -> E. y e. ( _Left ` A ) ( -us ` y ) = x ) )
36 leftold 
 |-  ( y e. ( _Left ` A ) -> y e. ( _Old ` ( bday ` A ) ) )
37 36 adantl 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> y e. ( _Old ` ( bday ` A ) ) )
38 leftno 
 |-  ( y e. ( _Left ` A ) -> y e. No )
39 38 adantl 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> y e. No )
40 oldbday 
 |-  ( ( ( bday ` A ) e. On /\ y e. No ) -> ( y e. ( _Old ` ( bday ` A ) ) <-> ( bday ` y ) e. ( bday ` A ) ) )
41 16 39 40 sylancr 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( y e. ( _Old ` ( bday ` A ) ) <-> ( bday ` y ) e. ( bday ` A ) ) )
42 37 41 mpbid 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( bday ` y ) e. ( bday ` A ) )
43 negbday 
 |-  ( y e. No -> ( bday ` ( -us ` y ) ) = ( bday ` y ) )
44 39 43 syl 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( bday ` ( -us ` y ) ) = ( bday ` y ) )
45 12 adantr 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( bday ` ( -us ` A ) ) = ( bday ` A ) )
46 42 44 45 3eltr4d 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( bday ` ( -us ` y ) ) e. ( bday ` ( -us ` A ) ) )
47 39 negscld 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( -us ` y ) e. No )
48 oldbday 
 |-  ( ( ( bday ` ( -us ` A ) ) e. On /\ ( -us ` y ) e. No ) -> ( ( -us ` y ) e. ( _Old ` ( bday ` ( -us ` A ) ) ) <-> ( bday ` ( -us ` y ) ) e. ( bday ` ( -us ` A ) ) ) )
49 4 47 48 sylancr 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( ( -us ` y ) e. ( _Old ` ( bday ` ( -us ` A ) ) ) <-> ( bday ` ( -us ` y ) ) e. ( bday ` ( -us ` A ) ) ) )
50 46 49 mpbird 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( -us ` y ) e. ( _Old ` ( bday ` ( -us ` A ) ) ) )
51 leftlt 
 |-  ( y e. ( _Left ` A ) -> y
52 51 adantl 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> y
53 simpl 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> A e. No )
54 39 53 ltnegsd 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( y  ( -us ` A )
55 52 54 mpbid 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( -us ` A )
56 elright 
 |-  ( ( -us ` y ) e. ( _Right ` ( -us ` A ) ) <-> ( ( -us ` y ) e. ( _Old ` ( bday ` ( -us ` A ) ) ) /\ ( -us ` A )
57 50 55 56 sylanbrc 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( -us ` y ) e. ( _Right ` ( -us ` A ) ) )
58 eleq1 
 |-  ( ( -us ` y ) = x -> ( ( -us ` y ) e. ( _Right ` ( -us ` A ) ) <-> x e. ( _Right ` ( -us ` A ) ) ) )
59 57 58 syl5ibcom 
 |-  ( ( A e. No /\ y e. ( _Left ` A ) ) -> ( ( -us ` y ) = x -> x e. ( _Right ` ( -us ` A ) ) ) )
60 59 rexlimdva 
 |-  ( A e. No -> ( E. y e. ( _Left ` A ) ( -us ` y ) = x -> x e. ( _Right ` ( -us ` A ) ) ) )
61 35 60 impbid 
 |-  ( A e. No -> ( x e. ( _Right ` ( -us ` A ) ) <-> E. y e. ( _Left ` A ) ( -us ` y ) = x ) )
62 negsfn 
 |-  -us Fn No
63 leftssno 
 |-  ( _Left ` A ) C_ No
64 fvelimab 
 |-  ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( x e. ( -us " ( _Left ` A ) ) <-> E. y e. ( _Left ` A ) ( -us ` y ) = x ) )
65 62 63 64 mp2an 
 |-  ( x e. ( -us " ( _Left ` A ) ) <-> E. y e. ( _Left ` A ) ( -us ` y ) = x )
66 61 65 bitr4di 
 |-  ( A e. No -> ( x e. ( _Right ` ( -us ` A ) ) <-> x e. ( -us " ( _Left ` A ) ) ) )
67 66 eqrdv 
 |-  ( A e. No -> ( _Right ` ( -us ` A ) ) = ( -us " ( _Left ` A ) ) )