Metamath Proof Explorer

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

Proof

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