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	⊢ ( 𝐴 ∈ No → ( L ‘ ( -us ‘ 𝐴 ) ) = ( -us “ ( R ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑦 = ( -us ‘ 𝑥 ) → ( ( -us ‘ 𝑦 ) = 𝑥 ↔ ( -us ‘ ( -us ‘ 𝑥 ) ) = 𝑥 ) )
2		leftno	⊢ ( 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) → 𝑥 ∈ No )
3	2	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → 𝑥 ∈ No )
4		negbday	⊢ ( 𝑥 ∈ No → ( bday ‘ ( -us ‘ 𝑥 ) ) = ( bday ‘ 𝑥 ) )
5	3 4	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝑥 ) ) = ( bday ‘ 𝑥 ) )
6		leftold	⊢ ( 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) → 𝑥 ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
7	6	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → 𝑥 ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
8		bdayon	⊢ ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ On
9		oldbday	⊢ ( ( ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ On ∧ 𝑥 ∈ No ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
10	8 3 9	sylancr	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( 𝑥 ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) ↔ ( bday ‘ 𝑥 ) ∈ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
11	7 10	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ ( -us ‘ 𝐴 ) ) )
12		negbday	⊢ ( 𝐴 ∈ No → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
13	12	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
14	11 13	eleqtrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday ‘ 𝐴 ) )
15	5 14	eqeltrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝑥 ) ) ∈ ( bday ‘ 𝐴 ) )
16		bdayon	⊢ ( bday ‘ 𝐴 ) ∈ On
17	3	negscld	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ 𝑥 ) ∈ No )
18		oldbday	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( -us ‘ 𝑥 ) ∈ No ) → ( ( -us ‘ 𝑥 ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( -us ‘ 𝑥 ) ) ∈ ( bday ‘ 𝐴 ) ) )
19	16 17 18	sylancr	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝑥 ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( -us ‘ 𝑥 ) ) ∈ ( bday ‘ 𝐴 ) ) )
20	15 19	mpbird	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ 𝑥 ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
21		negnegs	⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
22	21	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
23		leftlt	⊢ ( 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) → 𝑥 <s ( -us ‘ 𝐴 ) )
24	23	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → 𝑥 <s ( -us ‘ 𝐴 ) )
25		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
26	25	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ 𝐴 ) ∈ No )
27	3 26	ltnegsd	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( 𝑥 <s ( -us ‘ 𝐴 ) ↔ ( -us ‘ ( -us ‘ 𝐴 ) ) <s ( -us ‘ 𝑥 ) ) )
28	24 27	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ ( -us ‘ 𝐴 ) ) <s ( -us ‘ 𝑥 ) )
29	22 28	eqbrtrrd	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → 𝐴 <s ( -us ‘ 𝑥 ) )
30		elright	⊢ ( ( -us ‘ 𝑥 ) ∈ ( R ‘ 𝐴 ) ↔ ( ( -us ‘ 𝑥 ) ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s ( -us ‘ 𝑥 ) ) )
31	20 29 30	sylanbrc	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ 𝑥 ) ∈ ( R ‘ 𝐴 ) )
32		negnegs	⊢ ( 𝑥 ∈ No → ( -us ‘ ( -us ‘ 𝑥 ) ) = 𝑥 )
33	3 32	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ( -us ‘ ( -us ‘ 𝑥 ) ) = 𝑥 )
34	1 31 33	rspcedvdw	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) → ∃ 𝑦 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑦 ) = 𝑥 )
35	34	ex	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) → ∃ 𝑦 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑦 ) = 𝑥 ) )
36		rightold	⊢ ( 𝑦 ∈ ( R ‘ 𝐴 ) → 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
37		rightno	⊢ ( 𝑦 ∈ ( R ‘ 𝐴 ) → 𝑦 ∈ No )
38		oldbday	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 𝑦 ∈ No ) → ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) )
39	16 37 38	sylancr	⊢ ( 𝑦 ∈ ( R ‘ 𝐴 ) → ( 𝑦 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) ) )
40	36 39	mpbid	⊢ ( 𝑦 ∈ ( R ‘ 𝐴 ) → ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) )
41	40	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( bday ‘ 𝑦 ) ∈ ( bday ‘ 𝐴 ) )
42	37	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → 𝑦 ∈ No )
43		negbday	⊢ ( 𝑦 ∈ No → ( bday ‘ ( -us ‘ 𝑦 ) ) = ( bday ‘ 𝑦 ) )
44	42 43	syl	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( bday ‘ ( -us ‘ 𝑦 ) ) = ( bday ‘ 𝑦 ) )
45	12	adantr	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( bday ‘ ( -us ‘ 𝐴 ) ) = ( bday ‘ 𝐴 ) )
46	41 44 45	3eltr4d	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( bday ‘ ( -us ‘ 𝑦 ) ) ∈ ( bday ‘ ( -us ‘ 𝐴 ) ) )
47	42	negscld	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝑦 ) ∈ No )
48		oldbday	⊢ ( ( ( bday ‘ ( -us ‘ 𝐴 ) ) ∈ On ∧ ( -us ‘ 𝑦 ) ∈ No ) → ( ( -us ‘ 𝑦 ) ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) ↔ ( bday ‘ ( -us ‘ 𝑦 ) ) ∈ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
49	8 47 48	sylancr	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( ( -us ‘ 𝑦 ) ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) ↔ ( bday ‘ ( -us ‘ 𝑦 ) ) ∈ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
50	46 49	mpbird	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝑦 ) ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) )
51		rightgt	⊢ ( 𝑦 ∈ ( R ‘ 𝐴 ) → 𝐴 <s 𝑦 )
52	51	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → 𝐴 <s 𝑦 )
53		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → 𝐴 ∈ No )
54	53 42	ltnegsd	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( 𝐴 <s 𝑦 ↔ ( -us ‘ 𝑦 ) <s ( -us ‘ 𝐴 ) ) )
55	52 54	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝐴 ) )
56		elleft	⊢ ( ( -us ‘ 𝑦 ) ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ↔ ( ( -us ‘ 𝑦 ) ∈ ( O ‘ ( bday ‘ ( -us ‘ 𝐴 ) ) ) ∧ ( -us ‘ 𝑦 ) <s ( -us ‘ 𝐴 ) ) )
57	50 55 56	sylanbrc	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝑦 ) ∈ ( L ‘ ( -us ‘ 𝐴 ) ) )
58		eleq1	⊢ ( ( -us ‘ 𝑦 ) = 𝑥 → ( ( -us ‘ 𝑦 ) ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ↔ 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) )
59	57 58	syl5ibcom	⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ ( R ‘ 𝐴 ) ) → ( ( -us ‘ 𝑦 ) = 𝑥 → 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) )
60	59	rexlimdva	⊢ ( 𝐴 ∈ No → ( ∃ 𝑦 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑦 ) = 𝑥 → 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ) )
61	35 60	impbid	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ↔ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑦 ) = 𝑥 ) )
62		negsfn	⊢ -us Fn No
63		rightssno	⊢ ( R ‘ 𝐴 ) ⊆ No
64		fvelimab	⊢ ( ( -us Fn No ∧ ( R ‘ 𝐴 ) ⊆ No ) → ( 𝑥 ∈ ( -us “ ( R ‘ 𝐴 ) ) ↔ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑦 ) = 𝑥 ) )
65	62 63 64	mp2an	⊢ ( 𝑥 ∈ ( -us “ ( R ‘ 𝐴 ) ) ↔ ∃ 𝑦 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑦 ) = 𝑥 )
66	61 65	bitr4di	⊢ ( 𝐴 ∈ No → ( 𝑥 ∈ ( L ‘ ( -us ‘ 𝐴 ) ) ↔ 𝑥 ∈ ( -us “ ( R ‘ 𝐴 ) ) ) )
67	66	eqrdv	⊢ ( 𝐴 ∈ No → ( L ‘ ( -us ‘ 𝐴 ) ) = ( -us “ ( R ‘ 𝐴 ) ) )