Theorem onsbnd2

Description: The surreals of a given birthday are bounded below by the negative of that ordinal. (Contributed by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Assertion	onsbnd2	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(A\right){\le }_{s}B$$

Proof

Step	Hyp	Ref	Expression
1		madessno	$$⊢M\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{No}$$
2	1	sseli	$$⊢B\in M\left(\mathrm{bday}\left(A\right)\right)\to B\in \mathrm{No}$$
3	2	adantl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to B\in \mathrm{No}$$
4		negsbday	$$⊢B\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(B\right)\right)=\mathrm{bday}\left(B\right)$$
5	3 4	syl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left({+}_s\left(B\right)\right)=\mathrm{bday}\left(B\right)$$
6		madebdayim	$$⊢B\in M\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(B\right)\subseteq \mathrm{bday}\left(A\right)$$
7	6	adantl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left(B\right)\subseteq \mathrm{bday}\left(A\right)$$
8	5 7	eqsstrd	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left({+}_s\left(B\right)\right)\subseteq \mathrm{bday}\left(A\right)$$
9		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
10	3	negscld	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(B\right)\in \mathrm{No}$$
11		madebday	$$⊢\left(\mathrm{bday}\left(A\right)\in \mathrm{On}\wedge {+}_s\left(B\right)\in \mathrm{No}\right)\to \left({+}_s\left(B\right)\in M\left(\mathrm{bday}\left(A\right)\right)\leftrightarrow \mathrm{bday}\left({+}_s\left(B\right)\right)\subseteq \mathrm{bday}\left(A\right)\right)$$
12	9 10 11	sylancr	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \left({+}_s\left(B\right)\in M\left(\mathrm{bday}\left(A\right)\right)\leftrightarrow \mathrm{bday}\left({+}_s\left(B\right)\right)\subseteq \mathrm{bday}\left(A\right)\right)$$
13	8 12	mpbird	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(B\right)\in M\left(\mathrm{bday}\left(A\right)\right)$$
14		onsbnd	$$⊢\left(A\in {On}_s\wedge {+}_s\left(B\right)\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(B\right){\le }_{s}A$$
15	13 14	syldan	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(B\right){\le }_{s}A$$
16		onsno	$$⊢A\in {On}_s\to A\in \mathrm{No}$$
17	16	adantr	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to A\in \mathrm{No}$$
18	17	negscld	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(A\right)\in \mathrm{No}$$
19	18 3	slenegd	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \left({+}_s\left(A\right){\le }_{s}B\leftrightarrow {+}_s\left(B\right){\le }_s{+}_s\left({+}_s\left(A\right)\right)\right)$$
20		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
21	17 20	syl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left({+}_s\left(A\right)\right)=A$$
22	21	breq2d	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \left({+}_s\left(B\right){\le }_s{+}_s\left({+}_s\left(A\right)\right)\leftrightarrow {+}_s\left(B\right){\le }_{s}A\right)$$
23	19 22	bitr2d	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \left({+}_s\left(B\right){\le }_{s}A\leftrightarrow {+}_s\left(A\right){\le }_{s}B\right)$$
24	15 23	mpbid	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to {+}_s\left(A\right){\le }_{s}B$$