Theorem bdaybndex

Description: Bounds formed from the birthday are surreal numbers. (Contributed by RP, 21-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\right)\to B=\mathrm{bday}\left(A\right)$$
2		bdayval	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$
3	2	adantr	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$
4	1 3	eqtrd	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\right)\to B=\mathrm{dom}A$$
5		nodmon	$$⊢A\in \mathrm{No}\to \mathrm{dom}A\in \mathrm{On}$$
6	5	adantr	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\right)\to \mathrm{dom}A\in \mathrm{On}$$
7	4 6	eqeltrd	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\right)\to B\in \mathrm{On}$$
8		onnoxpg	$$⊢\left(B\in \mathrm{On}\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to B\times \left\{C\right\}\in \mathrm{No}$$
9	7 8	stoic3	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to B\times \left\{C\right\}\in \mathrm{No}$$