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

Proof

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