Theorem fvnobday

Description: The value of a surreal at its birthday is (/) . (Contributed by Scott Fenton, 14-Jun-2011) (Proof shortened by SF, 14-Apr-2012)

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

Proof

Step	Hyp	Ref	Expression
1		bdayval	$$⊢A\in \mathrm{No}\to \mathrm{bday}\left(A\right)=\mathrm{dom}A$$
2		nodmord	$$⊢A\in \mathrm{No}\to \mathrm{Ord}\mathrm{dom}A$$
3		ordirr	$$⊢\mathrm{Ord}\mathrm{dom}A\to \neg \mathrm{dom}A\in \mathrm{dom}A$$
4	2 3	syl	$$⊢A\in \mathrm{No}\to \neg \mathrm{dom}A\in \mathrm{dom}A$$
5	1 4	eqneltrd	$$⊢A\in \mathrm{No}\to \neg \mathrm{bday}\left(A\right)\in \mathrm{dom}A$$
6		ndmfv	$$⊢\neg \mathrm{bday}\left(A\right)\in \mathrm{dom}A\to A\left(\mathrm{bday}\left(A\right)\right)=\varnothing$$
7	5 6	syl	$$⊢A\in \mathrm{No}\to A\left(\mathrm{bday}\left(A\right)\right)=\varnothing$$