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

Proof

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

Metamath Proof Explorer

Theorem negsleft

Proof