Metamath Proof Explorer

Theorem negsleft

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