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		madeno	$$⊢B\in M\left(\mathrm{bday}\left(A\right)\right)\to B\in \mathrm{No}$$
2	1	adantl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to B\in \mathrm{No}$$
3		negbday	$$⊢B\in \mathrm{No}\to \mathrm{bday}\left({+}_s\left(B\right)\right)=\mathrm{bday}\left(B\right)$$
4	2 3	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)$$
5		madebdayim	$$⊢B\in M\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(B\right)\subseteq \mathrm{bday}\left(A\right)$$
6	5	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)$$
7	4 6	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)$$
8		bdayon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
9	2	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}$$
10		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)$$
11	8 9 10	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)$$
12	7 11	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)$$
13		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$$
14	12 13	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$$
15		onno	$$⊢A\in {On}_s\to A\in \mathrm{No}$$
16	15	adantr	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to A\in \mathrm{No}$$
17	16	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}$$
18	17 2	lenegsd	$$⊢\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)$$
19		negnegs	$$⊢A\in \mathrm{No}\to {+}_s\left({+}_s\left(A\right)\right)=A$$
20	16 19	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$$
21	20	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)$$
22	18 21	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)$$
23	14 22	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$$