Theorem onslt

Description: Less-than is the same as birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 7-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		onsno	⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
2		onnolt	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵 ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )
3	2	3expia	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ No ) → ( 𝐴 <s 𝐵 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 <s 𝐵 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
5		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
6		onsno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
7	6	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 ∈ No )
8		oldbday	⊢ ( ( ( bday ‘ 𝐵 ) ∈ On ∧ 𝐴 ∈ No ) → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ↔ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
9	5 7 8	sylancr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ↔ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
10		onsleft	⊢ ( 𝐵 ∈ Ons → ( O ‘ ( bday ‘ 𝐵 ) ) = ( L ‘ 𝐵 ) )
11	10	eleq2d	⊢ ( 𝐵 ∈ Ons → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ↔ 𝐴 ∈ ( L ‘ 𝐵 ) ) )
12	11	adantl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ↔ 𝐴 ∈ ( L ‘ 𝐵 ) ) )
13	9 12	bitr3d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ↔ 𝐴 ∈ ( L ‘ 𝐵 ) ) )
14		leftlt	⊢ ( 𝐴 ∈ ( L ‘ 𝐵 ) → 𝐴 <s 𝐵 )
15	13 14	biimtrdi	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) → 𝐴 <s 𝐵 ) )
16	4 15	impbid	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 <s 𝐵 ↔ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )