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

Metamath Proof Explorer

Theorem negright

Proof