Metamath Proof Explorer

Theorem negsright

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