Theorem bdayval

Description: The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011)

	Ref	Expression
Assertion	bdayval	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		dmexg	$$⊢A\in \mathrm{No}\to \mathrm{dom}A\in \mathrm{V}$$
2		dmeq	$$⊢x=A\to \mathrm{dom}x=\mathrm{dom}A$$
3		df-bday	$$⊢\mathrm{bday}=\left(x\in \mathrm{No}⟼\mathrm{dom}x\right)$$
4	2 3	fvmptg	$$⊢\left(A\in \mathrm{No}\wedge \mathrm{dom}A\in \mathrm{V}\right)\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$
5	1 4	mpdan	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$