negright - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > negright		Structured version Visualization version GIF version

Theorem negright 28450

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.)

**Assertion**
Ref	Expression
negright	⊢ (𝐴 ∈ No → (R‘( -_s‘𝐴)) = ( -_s “ (L‘𝐴)))

Proof of Theorem negright Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveqeq2 6894	. . . . . 6 ⊢ (𝑦 = ( -_s‘𝑥) → (( -_s‘𝑦) = 𝑥 ↔ ( -_s‘( -_s‘𝑥)) = 𝑥))
2		rightold 28267	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (R‘( -_s‘𝐴)) → 𝑥 ∈ (O‘(bday‘( -_s‘𝐴))))
3	2	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → 𝑥 ∈ (O‘(bday‘( -_s‘𝐴))))
4		bdayon 28143	. . . . . . . . . . 11 ⊢ (bday‘( -_s‘𝐴)) ∈ On
5		rightno 28269	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (R‘( -_s‘𝐴)) → 𝑥 ∈ No)
6	5	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → 𝑥 ∈ No)
7		oldbday 28292	. . . . . . . . . . 11 ⊢ (((bday‘( -_s‘𝐴)) ∈ On ∧ 𝑥 ∈ No) → (𝑥 ∈ (O‘(bday‘( -_s‘𝐴))) ↔ (bday‘𝑥) ∈ (bday‘( -_s‘𝐴))))
8	4, 6, 7	sylancr 599	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (𝑥 ∈ (O‘(bday‘( -_s‘𝐴))) ↔ (bday‘𝑥) ∈ (bday‘( -_s‘𝐴))))
9	3, 8	mpbid 235	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (bday‘𝑥) ∈ (bday‘( -_s‘𝐴)))
10		negbday 28448	. . . . . . . . . 10 ⊢ (𝑥 ∈ No → (bday‘( -_s‘𝑥)) = (bday‘𝑥))
11	6, 10	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (bday‘( -_s‘𝑥)) = (bday‘𝑥))
12		negbday 28448	. . . . . . . . . . 11 ⊢ (𝐴 ∈ No → (bday‘( -_s‘𝐴)) = (bday‘𝐴))
13	12	adantr 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (bday‘( -_s‘𝐴)) = (bday‘𝐴))
14	13	eqcomd 2766	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (bday‘𝐴) = (bday‘( -_s‘𝐴)))
15	9, 11, 14	3eltr4d 2875	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (bday‘( -_s‘𝑥)) ∈ (bday‘𝐴))
16		bdayon 28143	. . . . . . . . 9 ⊢ (bday‘𝐴) ∈ On
17	6	negscld 28428	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝑥) ∈ No)
18		oldbday 28292	. . . . . . . . 9 ⊢ (((bday‘𝐴) ∈ On ∧ ( -_s‘𝑥) ∈ No) → (( -_s‘𝑥) ∈ (O‘(bday‘𝐴)) ↔ (bday‘( -_s‘𝑥)) ∈ (bday‘𝐴)))
19	16, 17, 18	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (( -_s‘𝑥) ∈ (O‘(bday‘𝐴)) ↔ (bday‘( -_s‘𝑥)) ∈ (bday‘𝐴)))
20	15, 19	mpbird 260	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝑥) ∈ (O‘(bday‘𝐴)))
21		rightgt 28245	. . . . . . . . . 10 ⊢ (𝑥 ∈ (R‘( -_s‘𝐴)) → ( -_s‘𝐴) <s 𝑥)
22	21	adantl 487	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝐴) <s 𝑥)
23		simpl 488	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → 𝐴 ∈ No)
24	23	negscld 28428	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝐴) ∈ No)
25	24, 6	ltnegsd 28438	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → (( -_s‘𝐴) <s 𝑥 ↔ ( -_s‘𝑥) <s ( -_s‘( -_s‘𝐴))))
26	22, 25	mpbid 235	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝑥) <s ( -_s‘( -_s‘𝐴)))
27		negnegs 28435	. . . . . . . . 9 ⊢ (𝐴 ∈ No → ( -_s‘( -_s‘𝐴)) = 𝐴)
28	27	adantr 486	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘( -_s‘𝐴)) = 𝐴)
29	26, 28	breqtrd 5130	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝑥) <s 𝐴)
30		elleft 28242	. . . . . . 7 ⊢ (( -_s‘𝑥) ∈ (L‘𝐴) ↔ (( -_s‘𝑥) ∈ (O‘(bday‘𝐴)) ∧ ( -_s‘𝑥) <s 𝐴))
31	20, 29, 30	sylanbrc 595	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘𝑥) ∈ (L‘𝐴))
32		negnegs 28435	. . . . . . 7 ⊢ (𝑥 ∈ No → ( -_s‘( -_s‘𝑥)) = 𝑥)
33	6, 32	syl 18	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ( -_s‘( -_s‘𝑥)) = 𝑥)
34	1, 31, 33	rspcedvdw 3579	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ (R‘( -_s‘𝐴))) → ∃𝑦 ∈ (L‘𝐴)( -_s‘𝑦) = 𝑥)
35	34	ex 418	. . . 4 ⊢ (𝐴 ∈ No → (𝑥 ∈ (R‘( -_s‘𝐴)) → ∃𝑦 ∈ (L‘𝐴)( -_s‘𝑦) = 𝑥))
36		leftold 28266	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (L‘𝐴) → 𝑦 ∈ (O‘(bday‘𝐴)))
37	36	adantl 487	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → 𝑦 ∈ (O‘(bday‘𝐴)))
38		leftno 28268	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (L‘𝐴) → 𝑦 ∈ No)
39	38	adantl 487	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → 𝑦 ∈ No)
40		oldbday 28292	. . . . . . . . . . 11 ⊢ (((bday‘𝐴) ∈ On ∧ 𝑦 ∈ No) → (𝑦 ∈ (O‘(bday‘𝐴)) ↔ (bday‘𝑦) ∈ (bday‘𝐴)))
41	16, 39, 40	sylancr 599	. . . . . . . . . 10 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (𝑦 ∈ (O‘(bday‘𝐴)) ↔ (bday‘𝑦) ∈ (bday‘𝐴)))
42	37, 41	mpbid 235	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (bday‘𝑦) ∈ (bday‘𝐴))
43		negbday 28448	. . . . . . . . . 10 ⊢ (𝑦 ∈ No → (bday‘( -_s‘𝑦)) = (bday‘𝑦))
44	39, 43	syl 18	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (bday‘( -_s‘𝑦)) = (bday‘𝑦))
45	12	adantr 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (bday‘( -_s‘𝐴)) = (bday‘𝐴))
46	42, 44, 45	3eltr4d 2875	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (bday‘( -_s‘𝑦)) ∈ (bday‘( -_s‘𝐴)))
47	39	negscld 28428	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → ( -_s‘𝑦) ∈ No)
48		oldbday 28292	. . . . . . . . 9 ⊢ (((bday‘( -_s‘𝐴)) ∈ On ∧ ( -_s‘𝑦) ∈ No) → (( -_s‘𝑦) ∈ (O‘(bday‘( -_s‘𝐴))) ↔ (bday‘( -_s‘𝑦)) ∈ (bday‘( -_s‘𝐴))))
49	4, 47, 48	sylancr 599	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (( -_s‘𝑦) ∈ (O‘(bday‘( -_s‘𝐴))) ↔ (bday‘( -_s‘𝑦)) ∈ (bday‘( -_s‘𝐴))))
50	46, 49	mpbird 260	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → ( -_s‘𝑦) ∈ (O‘(bday‘( -_s‘𝐴))))
51		leftlt 28244	. . . . . . . . 9 ⊢ (𝑦 ∈ (L‘𝐴) → 𝑦 <s 𝐴)
52	51	adantl 487	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → 𝑦 <s 𝐴)
53		simpl 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → 𝐴 ∈ No)
54	39, 53	ltnegsd 28438	. . . . . . . 8 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (𝑦 <s 𝐴 ↔ ( -_s‘𝐴) <s ( -_s‘𝑦)))
55	52, 54	mpbid 235	. . . . . . 7 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → ( -_s‘𝐴) <s ( -_s‘𝑦))
56		elright 28243	. . . . . . 7 ⊢ (( -_s‘𝑦) ∈ (R‘( -_s‘𝐴)) ↔ (( -_s‘𝑦) ∈ (O‘(bday‘( -_s‘𝐴))) ∧ ( -_s‘𝐴) <s ( -_s‘𝑦)))
57	50, 55, 56	sylanbrc 595	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → ( -_s‘𝑦) ∈ (R‘( -_s‘𝐴)))
58		eleq1 2848	. . . . . 6 ⊢ (( -_s‘𝑦) = 𝑥 → (( -_s‘𝑦) ∈ (R‘( -_s‘𝐴)) ↔ 𝑥 ∈ (R‘( -_s‘𝐴))))
59	57, 58	syl5ibcom 248	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝑦 ∈ (L‘𝐴)) → (( -_s‘𝑦) = 𝑥 → 𝑥 ∈ (R‘( -_s‘𝐴))))
60	59	rexlimdva 3163	. . . 4 ⊢ (𝐴 ∈ No → (∃𝑦 ∈ (L‘𝐴)( -_s‘𝑦) = 𝑥 → 𝑥 ∈ (R‘( -_s‘𝐴))))
61	35, 60	impbid 215	. . 3 ⊢ (𝐴 ∈ No → (𝑥 ∈ (R‘( -_s‘𝐴)) ↔ ∃𝑦 ∈ (L‘𝐴)( -_s‘𝑦) = 𝑥))
62		negsfn 28414	. . . 4 ⊢ -_s Fn No
63		leftssno 28264	. . . 4 ⊢ (L‘𝐴) ⊆ No
64		fvelimab 6957	. . . 4 ⊢ (( -_s Fn No ∧ (L‘𝐴) ⊆ No) → (𝑥 ∈ ( -_s “ (L‘𝐴)) ↔ ∃𝑦 ∈ (L‘𝐴)( -_s‘𝑦) = 𝑥))
65	62, 63, 64	mp2an 705	. . 3 ⊢ (𝑥 ∈ ( -_s “ (L‘𝐴)) ↔ ∃𝑦 ∈ (L‘𝐴)( -_s‘𝑦) = 𝑥)
66	61, 65	bitr4di 292	. 2 ⊢ (𝐴 ∈ No → (𝑥 ∈ (R‘( -_s‘𝐴)) ↔ 𝑥 ∈ ( -_s “ (L‘𝐴))))
67	66	eqrdv 2758	1 ⊢ (𝐴 ∈ No → (R‘( -_s‘𝐴)) = ( -_s “ (L‘𝐴)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 ⊆ wss 3895 class class class wbr 5102 “ cima 5653 Oncon0 6362 Fn wfn 6533 ‘cfv 6538 Nocsur 28002 <s clts 28003 bdaycbday 28004 Ocold 28214 Lcleft 28216 Rcright 28217 -_scnegs 28410

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-ot 4858 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-1st 8001 df-2nd 8002 df-frecs 8302 df-wrecs 8333 df-recs 8382 df-1o 8479 df-2o 8480 df-nadd 8678 df-no 28005 df-lts 28006 df-bday 28007 df-les 28107 df-slts 28149 df-cuts 28151 df-0s 28198 df-made 28218 df-old 28219 df-left 28221 df-right 28222 df-norec 28329 df-norec2 28340 df-adds 28351 df-negs 28412

This theorem is used by: (None)

W3C validator