Theorem onnobdayg

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

	Ref	Expression
Assertion	onnobdayg	$$⊢\left(A\in \mathrm{On}\wedge B\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{bday}\left(A\times \left\{B\right\}\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		onnoxpg	$$⊢\left(A\in \mathrm{On}\wedge B\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to A\times \left\{B\right\}\in \mathrm{No}$$
2		bdayval	$$⊢A\times \left\{B\right\}\in \mathrm{No}\to \mathrm{bday}\left(A\times \left\{B\right\}\right)=\mathrm{dom}\left(A\times \left\{B\right\}\right)$$
3	1 2	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{bday}\left(A\times \left\{B\right\}\right)=\mathrm{dom}\left(A\times \left\{B\right\}\right)$$
4		simpr	$$⊢\left(A\in \mathrm{On}\wedge B\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to B\in \left\{1_{𝑜},2_{𝑜}\right\}$$
5		snnzg	$$⊢B\in \left\{1_{𝑜},2_{𝑜}\right\}\to \left\{B\right\}\ne \varnothing$$
6		dmxp	$$⊢\left\{B\right\}\ne \varnothing \to \mathrm{dom}\left(A\times \left\{B\right\}\right)=A$$
7	4 5 6	3syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{dom}\left(A\times \left\{B\right\}\right)=A$$
8	3 7	eqtrd	$$⊢\left(A\in \mathrm{On}\wedge B\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{bday}\left(A\times \left\{B\right\}\right)=A$$