Metamath Proof Explorer

Theorem onles

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 onles ⊢ A ∈ On s ∧ B ∈ On s → A ≤ s B ↔ bday ⁡ A ⊆ bday ⁡ B

Proof

Step Hyp Ref Expression
1 onlts ⊢ B ∈ On s ∧ A ∈ On s → B < s A ↔ bday ⁡ B ∈ bday ⁡ A
2 1 ancoms ⊢ A ∈ On s ∧ B ∈ On s → B < s A ↔ bday ⁡ B ∈ bday ⁡ A
3 2 notbid ⊢ A ∈ On s ∧ B ∈ On s → ¬ B < s A ↔ ¬ bday ⁡ B ∈ bday ⁡ A
4 onno ⊢ A ∈ On s → A ∈ No
5 onno ⊢ B ∈ On s → B ∈ No
6 lenlts ⊢ A ∈ No ∧ B ∈ No → A ≤ s B ↔ ¬ B < s A
7 4 5 6 syl2an ⊢ A ∈ On s ∧ B ∈ On s → A ≤ s B ↔ ¬ B < s A
8 bdayon ⊢ bday ⁡ A ∈ On
9 bdayon ⊢ bday ⁡ B ∈ On
10 ontri1 ⊢ bday ⁡ A ∈ On ∧ bday ⁡ B ∈ On → bday ⁡ A ⊆ bday ⁡ B ↔ ¬ bday ⁡ B ∈ bday ⁡ A
11 8 9 10 mp2an ⊢ bday ⁡ A ⊆ bday ⁡ B ↔ ¬ bday ⁡ B ∈ bday ⁡ A
12 11 a1i ⊢ A ∈ On s ∧ B ∈ On s → bday ⁡ A ⊆ bday ⁡ B ↔ ¬ bday ⁡ B ∈ bday ⁡ A
13 3 7 12 3bitr4d ⊢ A ∈ On s ∧ B ∈ On s → A ≤ s B ↔ bday ⁡ A ⊆ bday ⁡ B