Theorem bdaybndbday

Description: Bounds formed from the birthday have the same birthday. (Contributed by RP, 30-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		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}$$
2		bdayval	$$⊢B\times \left\{C\right\}\in \mathrm{No}\to \mathrm{bday}\left(B\times \left\{C\right\}\right)=\mathrm{dom}\left(B\times \left\{C\right\}\right)$$
3	1 2	syl	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{bday}\left(B\times \left\{C\right\}\right)=\mathrm{dom}\left(B\times \left\{C\right\}\right)$$
4		simp3	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to C\in \left\{1_{𝑜},2_{𝑜}\right\}$$
5		snnzg	$$⊢C\in \left\{1_{𝑜},2_{𝑜}\right\}\to \left\{C\right\}\ne \varnothing$$
6		dmxp	$$⊢\left\{C\right\}\ne \varnothing \to \mathrm{dom}\left(B\times \left\{C\right\}\right)=B$$
7	4 5 6	3syl	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{dom}\left(B\times \left\{C\right\}\right)=B$$
8		simp2	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to B=\mathrm{bday}\left(A\right)$$
9	3 7 8	3eqtrd	$$⊢\left(A\in \mathrm{No}\wedge B=\mathrm{bday}\left(A\right)\wedge C\in \left\{1_{𝑜},2_{𝑜}\right\}\right)\to \mathrm{bday}\left(B\times \left\{C\right\}\right)=\mathrm{bday}\left(A\right)$$