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

Proof

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