Theorem onsbnd

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

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

Proof

Step	Hyp	Ref	Expression
1		ral0	Could not format A. xR e. (/) B
2	1	a1i	Could not format ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A. xR e. (/) B A. xR e. (/) B
3		leftssold	$$⊢L\left(B\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
4		bdayon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
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		oldss	$$⊢\left(\mathrm{bday}\left(A\right)\in \mathrm{On}\wedge \mathrm{bday}\left(B\right)\subseteq \mathrm{bday}\left(A\right)\right)\to \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
8	4 6 7	sylancr	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
9	3 8	sstrid	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to L\left(B\right)\subseteq \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
10		onleft	$$⊢A\in {On}_s\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)=L\left(A\right)$$
11	10	adantr	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)=L\left(A\right)$$
12	9 11	sseqtrd	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to L\left(B\right)\subseteq L\left(A\right)$$
13	12	sselda	Could not format ( ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) /\ yL e. ( _Left ` B ) ) -> yL e. ( _Left ` A ) ) : No typesetting found for |- ( ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) /\ yL e. ( _Left ` B ) ) -> yL e. ( _Left ` A ) ) with typecode |-
14		leftlt	Could not format ( yL e. ( _Left ` A ) -> yL yL
15	13 14	syl	Could not format ( ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) /\ yL e. ( _Left ` B ) ) -> yL yL
16	15	ralrimiva	Could not format ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A. yL e. ( _Left ` B ) yL A. yL e. ( _Left ` B ) yL
17		lltr	$$⊢L\left(B\right){\ll }_{s}R\left(B\right)$$
18	17	a1i	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to L\left(B\right){\ll }_{s}R\left(B\right)$$
19		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
20		fvex	$$⊢L\left(A\right)\in \mathrm{V}$$
21	20	elpw	$$⊢L\left(A\right)\in 𝒫\mathrm{No}\leftrightarrow L\left(A\right)\subseteq \mathrm{No}$$
22	19 21	mpbir	$$⊢L\left(A\right)\in 𝒫\mathrm{No}$$
23		nulsgts	$$⊢L\left(A\right)\in 𝒫\mathrm{No}\to L\left(A\right){\ll }_s\varnothing$$
24	22 23	mp1i	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to L\left(A\right){\ll }_s\varnothing$$
25		madeno	$$⊢B\in M\left(\mathrm{bday}\left(A\right)\right)\to B\in \mathrm{No}$$
26	25	adantl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to B\in \mathrm{No}$$
27		lrcut	$$⊢B\in \mathrm{No}\to L\left(B\right){|}_{s}R\left(B\right)=B$$
28	26 27	syl	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to L\left(B\right){|}_{s}R\left(B\right)=B$$
29	28	eqcomd	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to B=L\left(B\right){|}_{s}R\left(B\right)$$
30		oncutleft	$$⊢A\in {On}_s\to A=L\left(A\right){|}_s\varnothing$$
31	30	adantr	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to A=L\left(A\right){|}_s\varnothing$$
32	18 24 29 31	lesrecd	Could not format ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( B <_s A <-> ( A. xR e. (/) B ( B <_s A <-> ( A. xR e. (/) B
33	2 16 32	mpbir2and	$$⊢\left(A\in {On}_s\wedge B\in M\left(\mathrm{bday}\left(A\right)\right)\right)\to B{\le }_{s}A$$