negleft

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

Metamath Proof Explorer

Theorem negleft

Proof