Theorem onnolt

Description: If a surreal ordinal is less than a given surreal, then it is simpler. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	onnolt	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐵 ∈ No )
2		onsno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
3	2	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → 𝐴 ∈ No )
4	3	adantr	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐴 ∈ No )
5		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
6		simpr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → 𝐵 ∈ No )
7		oldbday	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ No ) → ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
8	5 6 7	sylancr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
9		onsleft	⊢ ( 𝐴 ∈ Ons → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
10	9	eleq2d	⊢ ( 𝐴 ∈ Ons → ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ 𝐵 ∈ ( L ‘ 𝐴 ) ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ 𝐵 ∈ ( L ‘ 𝐴 ) ) )
12	8 11	bitr3d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ↔ 𝐵 ∈ ( L ‘ 𝐴 ) ) )
13		leftlt	⊢ ( 𝐵 ∈ ( L ‘ 𝐴 ) → 𝐵 <s 𝐴 )
14	12 13	biimtrdi	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) → 𝐵 <s 𝐴 ) )
15	14	imp	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐵 <s 𝐴 )
16	1 4 15	sltled	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐵 ≤s 𝐴 )
17	16	ex	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) → 𝐵 ≤s 𝐴 ) )
18		leftssold	⊢ ( L ‘ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝐵 ) )
19		fveq2	⊢ ( ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) → ( O ‘ ( bday ‘ 𝐵 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
20	19	3ad2ant3	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( O ‘ ( bday ‘ 𝐵 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
21	9	3ad2ant1	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
22	20 21	eqtrd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( O ‘ ( bday ‘ 𝐵 ) ) = ( L ‘ 𝐴 ) )
23	18 22	sseqtrid	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( L ‘ 𝐵 ) ⊆ ( L ‘ 𝐴 ) )
24		simp2	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → 𝐵 ∈ No )
25	2	3ad2ant1	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → 𝐴 ∈ No )
26		simp3	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) )
27		slelss	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( 𝐵 ≤s 𝐴 ↔ ( L ‘ 𝐵 ) ⊆ ( L ‘ 𝐴 ) ) )
28	24 25 26 27	syl3anc	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → ( 𝐵 ≤s 𝐴 ↔ ( L ‘ 𝐵 ) ⊆ ( L ‘ 𝐴 ) ) )
29	23 28	mpbird	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → 𝐵 ≤s 𝐴 )
30	29	3expia	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) → 𝐵 ≤s 𝐴 ) )
31	17 30	jaod	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) → 𝐵 ≤s 𝐴 ) )
32		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
33	32 5	onsseli	⊢ ( ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) )
34		ontri1	⊢ ( ( ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) ↔ ¬ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
35	32 5 34	mp2an	⊢ ( ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) ↔ ¬ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )
36	33 35	bitr3i	⊢ ( ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) ↔ ¬ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )
37	36	a1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ∨ ( bday ‘ 𝐵 ) = ( bday ‘ 𝐴 ) ) ↔ ¬ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
38		slenlt	⊢ ( ( 𝐵 ∈ No ∧ 𝐴 ∈ No ) → ( 𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
39	6 3 38	syl2anc	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( 𝐵 ≤s 𝐴 ↔ ¬ 𝐴 <s 𝐵 ) )
40	31 37 39	3imtr3d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( ¬ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) → ¬ 𝐴 <s 𝐵 ) )
41	40	con4d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
42	41	3impia	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )