Theorem onnobdayg

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

	Ref	Expression
Assertion	onnobdayg	|- ( ( A e. On /\ B e. { 1o , 2o } ) -> ( bday ` ( A X. { B } ) ) = A )

Proof

Step	Hyp	Ref	Expression
1		onnog	|- ( ( A e. On /\ B e. { 1o , 2o } ) -> ( A X. { B } ) e. No )
2		bdayval	|- ( ( A X. { B } ) e. No -> ( bday ` ( A X. { B } ) ) = dom ( A X. { B } ) )
3	1 2	syl	|- ( ( A e. On /\ B e. { 1o , 2o } ) -> ( bday ` ( A X. { B } ) ) = dom ( A X. { B } ) )
4		simpr	|- ( ( A e. On /\ B e. { 1o , 2o } ) -> B e. { 1o , 2o } )
5		snnzg	|- ( B e. { 1o , 2o } -> { B } =/= (/) )
6		dmxp	|- ( { B } =/= (/) -> dom ( A X. { B } ) = A )
7	4 5 6	3syl	|- ( ( A e. On /\ B e. { 1o , 2o } ) -> dom ( A X. { B } ) = A )
8	3 7	eqtrd	|- ( ( A e. On /\ B e. { 1o , 2o } ) -> ( bday ` ( A X. { B } ) ) = A )