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	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐵 ) ) )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐵 ) ) )
3		onsleft	⊢ ( 𝐴 ∈ Ons → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( L ‘ 𝐴 ) )
5		onsleft	⊢ ( 𝐵 ∈ Ons → ( O ‘ ( bday ‘ 𝐵 ) ) = ( L ‘ 𝐵 ) )
6	5	3ad2ant2	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( O ‘ ( bday ‘ 𝐵 ) ) = ( L ‘ 𝐵 ) )
7	2 4 6	3eqtr3d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( L ‘ 𝐴 ) = ( L ‘ 𝐵 ) )
8	7	oveq1d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( ( L ‘ 𝐴 ) |s ∅ ) = ( ( L ‘ 𝐵 ) |s ∅ ) )
9		onscutleft	⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
10	9	3ad2ant1	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
11		onscutleft	⊢ ( 𝐵 ∈ Ons → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
12	11	3ad2ant2	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
13	8 10 12	3eqtr4d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐴 = 𝐵 )