Metamath Proof Explorer

Theorem negleft

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

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

Proof

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