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	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐵 ≤s 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ral0	⊢ ∀ 𝑥𝑅 ∈ ∅ 𝐵 <s 𝑥𝑅
2	1	a1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ∀ 𝑥𝑅 ∈ ∅ 𝐵 <s 𝑥𝑅 )
3		leftssold	⊢ ( L ‘ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝐵 ) )
4		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
5		madebdayim	⊢ ( 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) )
6	5	adantl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) )
7		oldss	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) ) → ( O ‘ ( bday ‘ 𝐵 ) ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
8	4 6 7	sylancr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( O ‘ ( bday ‘ 𝐵 ) ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
9	3 8	sstrid	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( L ‘ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
10		onsleft	⊢ ( 𝐴 ∈ Ons → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
12	9 11	sseqtrd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( L ‘ 𝐵 ) ⊆ ( L ‘ 𝐴 ) )
13	12	sselda	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ) → 𝑦𝐿 ∈ ( L ‘ 𝐴 ) )
14		leftlt	⊢ ( 𝑦𝐿 ∈ ( L ‘ 𝐴 ) → 𝑦𝐿 <s 𝐴 )
15	13 14	syl	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) ∧ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) ) → 𝑦𝐿 <s 𝐴 )
16	15	ralrimiva	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ∀ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑦𝐿 <s 𝐴 )
17		lltropt	⊢ ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 )
18	17	a1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( L ‘ 𝐵 ) <<s ( R ‘ 𝐵 ) )
19		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
20		fvex	⊢ ( L ‘ 𝐴 ) ∈ V
21	20	elpw	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No ↔ ( L ‘ 𝐴 ) ⊆ No )
22	19 21	mpbir	⊢ ( L ‘ 𝐴 ) ∈ 𝒫 No
23		nulssgt	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No → ( L ‘ 𝐴 ) <<s ∅ )
24	22 23	mp1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( L ‘ 𝐴 ) <<s ∅ )
25		madessno	⊢ ( M ‘ ( bday ‘ 𝐴 ) ) ⊆ No
26	25	sseli	⊢ ( 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) → 𝐵 ∈ No )
27	26	adantl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐵 ∈ No )
28		lrcut	⊢ ( 𝐵 ∈ No → ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) = 𝐵 )
29	27 28	syl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) = 𝐵 )
30	29	eqcomd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐵 = ( ( L ‘ 𝐵 ) |s ( R ‘ 𝐵 ) ) )
31		onscutleft	⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
32	31	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
33	18 24 30 32	slerecd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝐵 ≤s 𝐴 ↔ ( ∀ 𝑥𝑅 ∈ ∅ 𝐵 <s 𝑥𝑅 ∧ ∀ 𝑦𝐿 ∈ ( L ‘ 𝐵 ) 𝑦𝐿 <s 𝐴 ) ) )
34	2 16 33	mpbir2and	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐵 ≤s 𝐴 )