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	$⊢ A \in No \to R (+_{s} (A)) = +_{s} [L (A)]$

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	$⊢ y = +_{s} (x) \to (+_{s} (y) = x \leftrightarrow +_{s} (+_{s} (x)) = x)$
2		rightssold	$⊢ R (+_{s} (A)) \subseteq Old (bday (+_{s} (A)))$
3	2	sseli	$⊢ x \in R (+_{s} (A)) \to x \in Old (bday (+_{s} (A)))$
4	3	adantl	$⊢ (A \in No \land x \in R (+_{s} (A))) \to x \in Old (bday (+_{s} (A)))$
5		bdayelon	$⊢ bday (+_{s} (A)) \in On$
6		rightssno	$⊢ R (+_{s} (A)) \subseteq No$
7	6	sseli	$⊢ x \in R (+_{s} (A)) \to x \in No$
8	7	adantl	$⊢ (A \in No \land x \in R (+_{s} (A))) \to x \in No$
9		oldbday	$⊢ (bday (+_{s} (A)) \in On \land x \in No) \to (x \in Old (bday (+_{s} (A))) \leftrightarrow bday (x) \in bday (+_{s} (A)))$
10	5 8 9	sylancr	$⊢ (A \in No \land x \in R (+_{s} (A))) \to (x \in Old (bday (+_{s} (A))) \leftrightarrow bday (x) \in bday (+_{s} (A)))$
11	4 10	mpbid	$⊢ (A \in No \land x \in R (+_{s} (A))) \to bday (x) \in bday (+_{s} (A))$
12		negsbday	$⊢ x \in No \to bday (+_{s} (x)) = bday (x)$
13	8 12	syl	$⊢ (A \in No \land x \in R (+_{s} (A))) \to bday (+_{s} (x)) = bday (x)$
14		negsbday	$⊢ A \in No \to bday (+_{s} (A)) = bday (A)$
15	14	adantr	$⊢ (A \in No \land x \in R (+_{s} (A))) \to bday (+_{s} (A)) = bday (A)$
16	15	eqcomd	$⊢ (A \in No \land x \in R (+_{s} (A))) \to bday (A) = bday (+_{s} (A))$
17	11 13 16	3eltr4d	$⊢ (A \in No \land x \in R (+_{s} (A))) \to bday (+_{s} (x)) \in bday (A)$
18		bdayelon	$⊢ bday (A) \in On$
19	8	negscld	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (x) \in No$
20		oldbday	$⊢ (bday (A) \in On \land +_{s} (x) \in No) \to (+_{s} (x) \in Old (bday (A)) \leftrightarrow bday (+_{s} (x)) \in bday (A))$
21	18 19 20	sylancr	$⊢ (A \in No \land x \in R (+_{s} (A))) \to (+_{s} (x) \in Old (bday (A)) \leftrightarrow bday (+_{s} (x)) \in bday (A))$
22	17 21	mpbird	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (x) \in Old (bday (A))$
23		rightgt	$⊢ x \in R (+_{s} (A)) \to +_{s} (A) <_{s} x$
24	23	adantl	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (A) <_{s} x$
25		simpl	$⊢ (A \in No \land x \in R (+_{s} (A))) \to A \in No$
26	25	negscld	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (A) \in No$
27	26 8	sltnegd	$⊢ (A \in No \land x \in R (+_{s} (A))) \to (+_{s} (A) <_{s} x \leftrightarrow +_{s} (x) <_{s} +_{s} (+_{s} (A)))$
28	24 27	mpbid	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (x) <_{s} +_{s} (+_{s} (A))$
29		negnegs	$⊢ A \in No \to +_{s} (+_{s} (A)) = A$
30	29	adantr	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (+_{s} (A)) = A$
31	28 30	breqtrd	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (x) <_{s} A$
32		elleft	$⊢ +_{s} (x) \in L (A) \leftrightarrow (+_{s} (x) \in Old (bday (A)) \land +_{s} (x) <_{s} A)$
33	22 31 32	sylanbrc	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (x) \in L (A)$
34		negnegs	$⊢ x \in No \to +_{s} (+_{s} (x)) = x$
35	8 34	syl	$⊢ (A \in No \land x \in R (+_{s} (A))) \to +_{s} (+_{s} (x)) = x$
36	1 33 35	rspcedvdw	$⊢ (A \in No \land x \in R (+_{s} (A))) \to \exists y \in L (A) +_{s} (y) = x$
37	36	ex	$⊢ A \in No \to (x \in R (+_{s} (A)) \to \exists y \in L (A) +_{s} (y) = x)$
38		leftssold	$⊢ L (A) \subseteq Old (bday (A))$
39	38	sseli	$⊢ y \in L (A) \to y \in Old (bday (A))$
40	39	adantl	$⊢ (A \in No \land y \in L (A)) \to y \in Old (bday (A))$
41		leftssno	$⊢ L (A) \subseteq No$
42	41	sseli	$⊢ y \in L (A) \to y \in No$
43	42	adantl	$⊢ (A \in No \land y \in L (A)) \to y \in No$
44		oldbday	$⊢ (bday (A) \in On \land y \in No) \to (y \in Old (bday (A)) \leftrightarrow bday (y) \in bday (A))$
45	18 43 44	sylancr	$⊢ (A \in No \land y \in L (A)) \to (y \in Old (bday (A)) \leftrightarrow bday (y) \in bday (A))$
46	40 45	mpbid	$⊢ (A \in No \land y \in L (A)) \to bday (y) \in bday (A)$
47		negsbday	$⊢ y \in No \to bday (+_{s} (y)) = bday (y)$
48	43 47	syl	$⊢ (A \in No \land y \in L (A)) \to bday (+_{s} (y)) = bday (y)$
49	14	adantr	$⊢ (A \in No \land y \in L (A)) \to bday (+_{s} (A)) = bday (A)$
50	46 48 49	3eltr4d	$⊢ (A \in No \land y \in L (A)) \to bday (+_{s} (y)) \in bday (+_{s} (A))$
51	43	negscld	$⊢ (A \in No \land y \in L (A)) \to +_{s} (y) \in No$
52		oldbday	$⊢ (bday (+_{s} (A)) \in On \land +_{s} (y) \in No) \to (+_{s} (y) \in Old (bday (+_{s} (A))) \leftrightarrow bday (+_{s} (y)) \in bday (+_{s} (A)))$
53	5 51 52	sylancr	$⊢ (A \in No \land y \in L (A)) \to (+_{s} (y) \in Old (bday (+_{s} (A))) \leftrightarrow bday (+_{s} (y)) \in bday (+_{s} (A)))$
54	50 53	mpbird	$⊢ (A \in No \land y \in L (A)) \to +_{s} (y) \in Old (bday (+_{s} (A)))$
55		leftlt	$⊢ y \in L (A) \to y <_{s} A$
56	55	adantl	$⊢ (A \in No \land y \in L (A)) \to y <_{s} A$
57		simpl	$⊢ (A \in No \land y \in L (A)) \to A \in No$
58	43 57	sltnegd	$⊢ (A \in No \land y \in L (A)) \to (y <_{s} A \leftrightarrow +_{s} (A) <_{s} +_{s} (y))$
59	56 58	mpbid	$⊢ (A \in No \land y \in L (A)) \to +_{s} (A) <_{s} +_{s} (y)$
60		elright	$⊢ +_{s} (y) \in R (+_{s} (A)) \leftrightarrow (+_{s} (y) \in Old (bday (+_{s} (A))) \land +_{s} (A) <_{s} +_{s} (y))$
61	54 59 60	sylanbrc	$⊢ (A \in No \land y \in L (A)) \to +_{s} (y) \in R (+_{s} (A))$
62		eleq1	$⊢ +_{s} (y) = x \to (+_{s} (y) \in R (+_{s} (A)) \leftrightarrow x \in R (+_{s} (A)))$
63	61 62	syl5ibcom	$⊢ (A \in No \land y \in L (A)) \to (+_{s} (y) = x \to x \in R (+_{s} (A)))$
64	63	rexlimdva	$⊢ A \in No \to (\exists y \in L (A) +_{s} (y) = x \to x \in R (+_{s} (A)))$
65	37 64	impbid	$⊢ A \in No \to (x \in R (+_{s} (A)) \leftrightarrow \exists y \in L (A) +_{s} (y) = x)$
66		negsfn	$⊢ +_{s} Fn No$
67		fvelimab	$⊢ (+_{s} Fn No \land L (A) \subseteq No) \to (x \in +_{s} [L (A)] \leftrightarrow \exists y \in L (A) +_{s} (y) = x)$
68	66 41 67	mp2an	$⊢ x \in +_{s} [L (A)] \leftrightarrow \exists y \in L (A) +_{s} (y) = x$
69	65 68	bitr4di	$⊢ A \in No \to (x \in R (+_{s} (A)) \leftrightarrow x \in +_{s} [L (A)])$
70	69	eqrdv	$⊢ A \in No \to R (+_{s} (A)) = +_{s} [L (A)]$

Metamath Proof Explorer

Theorem negsright

Proof