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

Proof

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