Theorem onnobdayg

Description: Every ordinal maps to a surreal number of that birthday. (Contributed by RP, 21-Sep-2023)

	Ref	Expression
Assertion	onnobdayg	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1o , 2o } ) → ( bday ‘ ( 𝐴 × { 𝐵 } ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		onnog	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1o , 2o } ) → ( 𝐴 × { 𝐵 } ) ∈ No )
2		bdayval	⊢ ( ( 𝐴 × { 𝐵 } ) ∈ No → ( bday ‘ ( 𝐴 × { 𝐵 } ) ) = dom ( 𝐴 × { 𝐵 } ) )
3	1 2	syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1o , 2o } ) → ( bday ‘ ( 𝐴 × { 𝐵 } ) ) = dom ( 𝐴 × { 𝐵 } ) )
4		simpr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1o , 2o } ) → 𝐵 ∈ { 1o , 2o } )
5		snnzg	⊢ ( 𝐵 ∈ { 1o , 2o } → { 𝐵 } ≠ ∅ )
6		dmxp	⊢ ( { 𝐵 } ≠ ∅ → dom ( 𝐴 × { 𝐵 } ) = 𝐴 )
7	4 5 6	3syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1o , 2o } ) → dom ( 𝐴 × { 𝐵 } ) = 𝐴 )
8	3 7	eqtrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ { 1o , 2o } ) → ( bday ‘ ( 𝐴 × { 𝐵 } ) ) = 𝐴 )