Theorem onsle

Description: Less-than or equal is the same as non-strict birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 25-Feb-2026)

	Ref	Expression
Assertion	onsle	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ≤s 𝐵 ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		onslt	⊢ ( ( 𝐵 ∈ Ons ∧ 𝐴 ∈ Ons ) → ( 𝐵 <s 𝐴 ↔ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐵 <s 𝐴 ↔ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
3	2	notbid	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ¬ 𝐵 <s 𝐴 ↔ ¬ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
4		onsno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
5		onsno	⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
6		slenlt	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
7	4 5 6	syl2an	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴 ) )
8		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
9		bdayelon	⊢ ( bday ‘ 𝐵 ) ∈ On
10		ontri1	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) ↔ ¬ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
11	8 9 10	mp2an	⊢ ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) ↔ ¬ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) )
12	11	a1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) ↔ ¬ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
13	3 7 12	3bitr4d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 ≤s 𝐵 ↔ ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) ) )