Metamath Proof Explorer

Theorem bday11on

Description: The birthday function is one-to-one over the surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025)

Ref Expression
Assertion bday11on ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → A = B

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ bday ⁡ A = bday ⁡ B → Old ⁡ bday ⁡ A = Old ⁡ bday ⁡ B
2 1 3ad2ant3 ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → Old ⁡ bday ⁡ A = Old ⁡ bday ⁡ B
3 onsleft ⊢ A ∈ On s → Old ⁡ bday ⁡ A = L ⁡ A
4 3 3ad2ant1 ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → Old ⁡ bday ⁡ A = L ⁡ A
5 onsleft ⊢ B ∈ On s → Old ⁡ bday ⁡ B = L ⁡ B
6 5 3ad2ant2 ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → Old ⁡ bday ⁡ B = L ⁡ B
7 2 4 6 3eqtr3d ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → L ⁡ A = L ⁡ B
8 7 oveq1d ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → L ⁡ A | s ∅ = L ⁡ B | s ∅
9 onscutleft ⊢ A ∈ On s → A = L ⁡ A | s ∅
10 9 3ad2ant1 ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → A = L ⁡ A | s ∅
11 onscutleft ⊢ B ∈ On s → B = L ⁡ B | s ∅
12 11 3ad2ant2 ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → B = L ⁡ B | s ∅
13 8 10 12 3eqtr4d ⊢ A ∈ On s ∧ B ∈ On s ∧ bday ⁡ A = bday ⁡ B → A = B